:: MSAFREE1 semantic presentation

begin

theorem Th1: :: MSAFREE1:1
for f, g being Function st g in product f holds
rng g c= Union f
proof
let f, g be Function; ::_thesis: ( g in product f implies rng g c= Union f )
assume A1: g in product f ; ::_thesis: rng g c= Union f
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in Union f )
assume  y in rng g ; ::_thesis: y in Union f
then consider x being set  such that
A2: x in dom g and
A3: y = g . x by FUNCT_1:def_3;
A4: dom g = dom f by A1, CARD_3:9;
then  y in f . x by A1, A2, A3, CARD_3:9;
hence  y in Union f by A4, A2, CARD_5:2; ::_thesis: verum
end;

scheme :: MSAFREE1:sch 1
DTConstrUniq{ F1() ->  non empty DTConstrStr , F2() ->  non empty set , F3( set ) ->  Element of F2(), F4( set , set , set ) ->  Element of F2(), F5() ->  Function of (TS F1()),F2(), F6() ->  Function of (TS F1()),F2() } :
 F5() = F6()
provided
A1: for t being Symbol of F1() st t in Terminals F1() holds
F5() . (root-tree t) = F3(t) and
A2: for nt being Symbol of F1()
for ts being Element of (TS F1()) * st nt ==> roots ts holds
for x being Element of F2() * st x = F5() * ts holds
F5() . (nt -tree ts) = F4(nt,ts,x) and
A3: for t being Symbol of F1() st t in Terminals F1() holds
F6() . (root-tree t) = F3(t) and
A4: for nt being Symbol of F1()
for ts being Element of (TS F1()) * st nt ==> roots ts holds
for x being Element of F2() * st x = F6() * ts holds
F6() . (nt -tree ts) = F4(nt,ts,x)
proof
defpred S1[ set ] means F5() . $1 = F6() . $1;
A5: for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts & ( for t being DecoratedTree of the carrier of F1() st t in rng ts holds
S1[t] ) holds
S1[nt -tree ts]
proof
let nt be Symbol of F1(); ::_thesis: for ts being FinSequence of TS F1() st nt ==> roots ts & ( for t being DecoratedTree of the carrier of F1() st t in rng ts holds
S1[t] ) holds
S1[nt -tree ts]
let ts be FinSequence of TS F1(); ::_thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of F1() st t in rng ts holds
S1[t] ) implies S1[nt -tree ts] )
assume that
A6: nt ==> roots ts and
A7: for t being DecoratedTree of the carrier of F1() st t in rng ts holds
F5() . t = F6() . t ; ::_thesis: S1[nt -tree ts]
A8: rng ts c= TS F1() by FINSEQ_1:def_4;
then A9: rng ts c= dom F5() by FUNCT_2:def_1;
then A10: dom (F5() * ts) = dom ts by RELAT_1:27;
 rng ts c= dom F6() by A8, FUNCT_2:def_1;
then A11: dom (F6() * ts) = dom ts by RELAT_1:27;
A12: now__::_thesis:_for_x_being_set_st_x_in_dom_ts_holds_
(F5()_*_ts)_._x_=_(F6()_*_ts)_._x
let x be set ; ::_thesis: ( x in dom ts implies (F5() * ts) . x = (F6() * ts) . x )
assume A13: x in dom ts ; ::_thesis: (F5() * ts) . x = (F6() * ts) . x
then reconsider t = ts . x as Element of FinTrees the carrier of F1() by DTCONSTR:2;
 t in rng ts by A13, FUNCT_1:def_3;
then A14: F5() . t = F6() . t by A7;
thus (F5() * ts) . x = F5() . t by A10, A13, FUNCT_1:12
.= (F6() * ts) . x by A11, A13, A14, FUNCT_1:12 ; ::_thesis: verum
end;
dom (F5() * ts) = dom ts by A9, RELAT_1:27
.= Seg (len ts) by FINSEQ_1:def_3 ;
then reconsider ntv1 = F5() * ts as FinSequence by FINSEQ_1:def_2;
 rng ntv1 c= F2() by RELAT_1:def_19;
then  ntv1 is FinSequence of F2() by FINSEQ_1:def_4;
then reconsider ntv1 = ntv1 as Element of F2() * by FINSEQ_1:def_11;
reconsider tss = ts as Element of (TS F1()) * by FINSEQ_1:def_11;
thus F5() . (nt -tree ts) = F4(nt,tss,ntv1) by A2, A6
.= F6() . (nt -tree ts) by A4, A6, A10, A11, A12, FUNCT_1:2 ; ::_thesis: verum
end;
A15: for s being Symbol of F1() st s in Terminals F1() holds
S1[ root-tree s]
proof
let s be Symbol of F1(); ::_thesis: ( s in Terminals F1() implies S1[ root-tree s] )
assume A16: s in Terminals F1() ; ::_thesis: S1[ root-tree s]
hence F5() . (root-tree s) = F3(s) by A1
.= F6() . (root-tree s) by A3, A16 ;
::_thesis: verum
end;
 for t being DecoratedTree of the carrier of F1() st t in TS F1() holds
S1[t] from DTCONSTR:sch_7(A15, A5);
then  for x being set st x in TS F1() holds
F5() . x = F6() . x ;
hence  F5() = F6() by FUNCT_2:12; ::_thesis: verum
end;

theorem Th2: :: MSAFREE1:2
for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S
for o, b being set st [o,b] in REL X holds
( o in [: the carrier' of S,{ the carrier of S}:] & b in ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for X being ManySortedSet of the carrier of S
for o, b being set st [o,b] in REL X holds
( o in [: the carrier' of S,{ the carrier of S}:] & b in ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * )
let X be ManySortedSet of the carrier of S; ::_thesis: for o, b being set st [o,b] in REL X holds
( o in [: the carrier' of S,{ the carrier of S}:] & b in ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * )
let o, b be set ; ::_thesis: ( [o,b] in REL X implies ( o in [: the carrier' of S,{ the carrier of S}:] & b in ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * ) )
assume A1: [o,b] in REL X ; ::_thesis: ( o in [: the carrier' of S,{ the carrier of S}:] & b in ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * )
then reconsider o9 = o as Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) by ZFMISC_1:87;
reconsider b9 = b as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by A1, ZFMISC_1:87;
A2: [o9,b9] in REL X by A1;
hence  o in [: the carrier' of S,{ the carrier of S}:] by MSAFREE:def_7; ::_thesis: b in ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *
thus  b in ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by A2; ::_thesis: verum
end;

theorem :: MSAFREE1:3
for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S
for o being OperSymbol of S
for b being FinSequence st [[o, the carrier of S],b] in REL X holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for X being ManySortedSet of the carrier of S
for o being OperSymbol of S
for b being FinSequence st [[o, the carrier of S],b] in REL X holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) )
let X be ManySortedSet of the carrier of S; ::_thesis: for o being OperSymbol of S
for b being FinSequence st [[o, the carrier of S],b] in REL X holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) )
let o be OperSymbol of S; ::_thesis: for b being FinSequence st [[o, the carrier of S],b] in REL X holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) )
let b be FinSequence; ::_thesis: ( [[o, the carrier of S],b] in REL X implies ( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) )
assume A1: [[o, the carrier of S],b] in REL X ; ::_thesis: ( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) )
then reconsider b9 = b as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by Th2;
 len b9 = len (the_arity_of o) by A1, MSAFREE:5;
hence  len b = len (the_arity_of o) ; ::_thesis: for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) )
 for x being set st x in dom b9 holds
( ( b9 . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b9 . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b9 . x in Union (coprod X) implies b9 . x in coprod (((the_arity_of o) . x),X) ) ) by A1, MSAFREE:5;
hence  for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ; ::_thesis: verum
end;

registration
let I be non empty set ;
let M be ManySortedSet of I;
cluster rng M ->  non empty ;
coherence
 not rng M is empty ;
end;

registration
let I be set ;
cluster Relation-like V3() I -defined Function-like total  ->  disjoint_valued for set ;
coherence
 for b1 being ManySortedSet of I st b1 is V3() holds
b1 is disjoint_valued
proof
let M be ManySortedSet of I; ::_thesis: ( M is V3() implies M is disjoint_valued )
assume A1: M is V3() ; ::_thesis: M is disjoint_valued
let x, y be set ; :: according to PROB_2:def_2 ::_thesis: ( x = y or M . x misses M . y )
assume  x <> y ; ::_thesis: M . x misses M . y
percases ( ( x in dom M & y in dom M ) or not x in dom M or not y in dom M ) ;
suppose ( x in dom M & y in dom M ) ; ::_thesis: M . x misses M . y
 M . x is empty by A1;
hence  M . x misses M . y by XBOOLE_1:65; ::_thesis: verum
end;
suppose ( not x in dom M or not y in dom M ) ; ::_thesis: M . x misses M . y
then  ( M . x = {} or M . y = {} ) by FUNCT_1:def_2;
hence  M . x misses M . y by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
end;

registration
let I be set ;
cluster Relation-like I -defined Function-like total disjoint_valued for set ;
existence
 ex b1 being ManySortedSet of I st b1 is disjoint_valued
proof
set M = the V3() ManySortedSet of I;
take  the V3() ManySortedSet of I ; ::_thesis: the V3() ManySortedSet of I is disjoint_valued
thus  the V3() ManySortedSet of I is disjoint_valued ; ::_thesis: verum
end;
end;

definition
let I be non empty set ;
let X be disjoint_valued ManySortedSet of I;
let D be V2() ManySortedSet of I;
let F be ManySortedFunction of X,D;
func Flatten F ->  Function of (Union X),(Union D) means :Def1: :: MSAFREE1:def 1
 for i being Element of I
for x being set st x in X . i holds
it . x = (F . i) . x;
existence
 ex b1 being Function of (Union X),(Union D) st
for i being Element of I
for x being set st x in X . i holds
b1 . x = (F . i) . x
proof
defpred S1[ set , set ] means  for i being Element of I st $1 in X . i holds
$2 = (F . i) . $1;
A1: for x being set st x in Union X holds
ex y being set st
( y in Union D & S1[x,y] )
proof
let e be set ; ::_thesis: ( e in Union X implies ex y being set st
( y in Union D & S1[e,y] ) )
assume  e in Union X ; ::_thesis: ex y being set st
( y in Union D & S1[e,y] )
then consider i being set  such that
A2: i in dom X and
A3: e in X . i by CARD_5:2;
reconsider i = i as Element of I by A2, PARTFUN1:def_2;
take u = (F . i) . e; ::_thesis: ( u in Union D & S1[e,u] )
 i in I ;
then A4: i in dom D by PARTFUN1:def_2;
 (F . i) . e in D . i by A3, FUNCT_2:5;
hence  u in Union D by A4, CARD_5:2; ::_thesis: S1[e,u]
let i9 be Element of I; ::_thesis: ( e in X . i9 implies u = (F . i9) . e )
assume  e in X . i9 ; ::_thesis: u = (F . i9) . e
then  X . i9 meets X . i by A3, XBOOLE_0:3;
hence  u = (F . i9) . e by PROB_2:def_2; ::_thesis: verum
end;
consider f being Function of (Union X),(Union D) such that
A5: for e being set st e in Union X holds
S1[e,f . e] from FUNCT_2:sch_1(A1);
take  f ; ::_thesis: for i being Element of I
for x being set st x in X . i holds
f . x = (F . i) . x
let i be Element of I; ::_thesis: for x being set st x in X . i holds
f . x = (F . i) . x
let x be set ; ::_thesis: ( x in X . i implies f . x = (F . i) . x )
assume A6: x in X . i ; ::_thesis: f . x = (F . i) . x
 i in I ;
then  i in dom X by PARTFUN1:def_2;
then  x in Union X by A6, CARD_5:2;
hence  f . x = (F . i) . x by A5, A6; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Function of (Union X),(Union D) st ( for i being Element of I
for x being set st x in X . i holds
b1 . x = (F . i) . x ) & ( for i being Element of I
for x being set st x in X . i holds
b2 . x = (F . i) . x ) holds
b1 = b2;
proof
let F1, F2 be Function of (Union X),(Union D); ::_thesis: ( ( for i being Element of I
for x being set st x in X . i holds
F1 . x = (F . i) . x ) & ( for i being Element of I
for x being set st x in X . i holds
F2 . x = (F . i) . x ) implies F1 = F2 )
assume that
A7: for i being Element of I
for x being set st x in X . i holds
F1 . x = (F . i) . x and
A8: for i being Element of I
for x being set st x in X . i holds
F2 . x = (F . i) . x ; ::_thesis: F1 = F2
now__::_thesis:_for_x_being_set_st_x_in_Union_X_holds_
F1_._x_=_F2_._x
let x be set ; ::_thesis: ( x in Union X implies F1 . x = F2 . x )
assume  x in Union X ; ::_thesis: F1 . x = F2 . x
then consider i being set  such that
A9: i in dom X and
A10: x in X . i by CARD_5:2;
reconsider i = i as Element of I by A9, PARTFUN1:def_2;
thus F1 . x = (F . i) . x by A7, A10
.= F2 . x by A8, A10 ; ::_thesis: verum
end;
hence  F1 = F2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines Flatten MSAFREE1:def_1_:_
 for I being non empty set
for X being disjoint_valued ManySortedSet of I
for D being V2() ManySortedSet of I
for F being ManySortedFunction of X,D
for b5 being Function of (Union X),(Union D) holds
( b5 = Flatten F iff for i being Element of I
for x being set st x in X . i holds
b5 . x = (F . i) . x );

theorem Th4: :: MSAFREE1:4
for I being non empty set
for X being disjoint_valued ManySortedSet of I
for D being V2() ManySortedSet of I
for F1, F2 being ManySortedFunction of X,D st Flatten F1 = Flatten F2 holds
F1 = F2
proof
let I be non empty set ; ::_thesis: for X being disjoint_valued ManySortedSet of I
for D being V2() ManySortedSet of I
for F1, F2 being ManySortedFunction of X,D st Flatten F1 = Flatten F2 holds
F1 = F2
let X be disjoint_valued ManySortedSet of I; ::_thesis: for D being V2() ManySortedSet of I
for F1, F2 being ManySortedFunction of X,D st Flatten F1 = Flatten F2 holds
F1 = F2
let D be V2() ManySortedSet of I; ::_thesis: for F1, F2 being ManySortedFunction of X,D st Flatten F1 = Flatten F2 holds
F1 = F2
let F1, F2 be ManySortedFunction of X,D; ::_thesis: ( Flatten F1 = Flatten F2 implies F1 = F2 )
assume A1: Flatten F1 = Flatten F2 ; ::_thesis: F1 = F2
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
F1_._i_=_F2_._i
let i be set ; ::_thesis: ( i in I implies F1 . i = F2 . i )
assume A2: i in I ; ::_thesis: F1 . i = F2 . i
then reconsider Di = D . i as non empty set ;
reconsider f1 = F1 . i, f2 = F2 . i as Function of (X . i),Di by A2, PBOOLE:def_15;
now__::_thesis:_for_x_being_set_st_x_in_X_._i_holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in X . i implies f1 . x = f2 . x )
assume A3: x in X . i ; ::_thesis: f1 . x = f2 . x
hence f1 . x = (Flatten F1) . x by A2, Def1
.= f2 . x by A1, A2, A3, Def1 ;
::_thesis: verum
end;
hence  F1 . i = F2 . i by FUNCT_2:12; ::_thesis: verum
end;
hence  F1 = F2 by PBOOLE:3; ::_thesis: verum
end;

definition
let S be non empty ManySortedSign ;
let A be MSAlgebra over S;
attrA is disjoint_valued  means :Def2: :: MSAFREE1:def 2
 the Sorts of A is disjoint_valued ;
end;

:: deftheorem Def2 defines disjoint_valued MSAFREE1:def_2_:_
 for S being non empty ManySortedSign
for A being MSAlgebra over S holds
( A is disjoint_valued iff the Sorts of A is disjoint_valued );

definition
let S be non empty ManySortedSign ;
func SingleAlg S ->  strict MSAlgebra over S means :Def3: :: MSAFREE1:def 3
 for i being set st i in the carrier of S holds
the Sorts of it . i = {i};
existence
 ex b1 being strict MSAlgebra over S st
for i being set st i in the carrier of S holds
the Sorts of b1 . i = {i}
proof
deffunc H1( set ) ->  set = {$1};
consider f being ManySortedSet of the carrier of S such that
A1: for i being set st i in the carrier of S holds
f . i = H1(i) from PBOOLE:sch_4();
set Ch = the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S;
take  MSAlgebra(# f, the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S #) ; ::_thesis: for i being set st i in the carrier of S holds
the Sorts of MSAlgebra(# f, the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S #) . i = {i}
thus  for i being set st i in the carrier of S holds
the Sorts of MSAlgebra(# f, the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S #) . i = {i} by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict MSAlgebra over S st ( for i being set st i in the carrier of S holds
the Sorts of b1 . i = {i} ) & ( for i being set st i in the carrier of S holds
the Sorts of b2 . i = {i} ) holds
b1 = b2
proof
let A1, A2 be strict MSAlgebra over S; ::_thesis: ( ( for i being set st i in the carrier of S holds
the Sorts of A1 . i = {i} ) & ( for i being set st i in the carrier of S holds
the Sorts of A2 . i = {i} ) implies A1 = A2 )
assume that
A2: for i being set st i in the carrier of S holds
the Sorts of A1 . i = {i} and
A3: for i being set st i in the carrier of S holds
the Sorts of A2 . i = {i} ; ::_thesis: A1 = A2
set B = the Sorts of A1;
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
the_Sorts_of_A1_._i_=_the_Sorts_of_A2_._i
let i be set ; ::_thesis: ( i in the carrier of S implies the Sorts of A1 . i = the Sorts of A2 . i )
assume A4: i in the carrier of S ; ::_thesis: the Sorts of A1 . i = the Sorts of A2 . i
hence  the Sorts of A1 . i = {i} by A2
.= the Sorts of A2 . i by A3, A4 ;
::_thesis: verum
end;
then A5: the Sorts of A1 = the Sorts of A2 by PBOOLE:3;
A6: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1;
now__::_thesis:_for_i_being_set_st_i_in_the_carrier'_of_S_holds_
the_Charact_of_A1_._i_=_the_Charact_of_A2_._i
let i be set ; ::_thesis: ( i in the carrier' of S implies the Charact of A1 . i = the Charact of A2 . i )
set A = ( the Sorts of A1 * the ResultSort of S) . i;
assume A7: i in the carrier' of S ; ::_thesis: the Charact of A1 . i = the Charact of A2 . i
then A8: ( the Sorts of A1 * the ResultSort of S) . i = the Sorts of A1 . ( the ResultSort of S . i) by A6, FUNCT_1:13
.= {( the ResultSort of S . i)} by A2, A7, FUNCT_2:5 ;
then reconsider A = ( the Sorts of A1 * the ResultSort of S) . i as non empty set ;
reconsider f1 = the Charact of A1 . i, f2 = the Charact of A2 . i as Function of ((( the Sorts of A1 #) * the Arity of S) . i),A by A5, A7, PBOOLE:def_15;
now__::_thesis:_for_x_being_set_st_x_in_((_the_Sorts_of_A1_#)_*_the_Arity_of_S)_._i_holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in (( the Sorts of A1 #) * the Arity of S) . i implies f1 . x = f2 . x )
assume A9: x in (( the Sorts of A1 #) * the Arity of S) . i ; ::_thesis: f1 . x = f2 . x
then  f1 . x in A by FUNCT_2:5;
then A10: f1 . x = the ResultSort of S . i by A8, TARSKI:def_1;
 f2 . x in A by A9, FUNCT_2:5;
hence  f1 . x = f2 . x by A8, A10, TARSKI:def_1; ::_thesis: verum
end;
hence  the Charact of A1 . i = the Charact of A2 . i by FUNCT_2:12; ::_thesis: verum
end;
hence  A1 = A2 by A5, PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines SingleAlg MSAFREE1:def_3_:_
 for S being non empty ManySortedSign
for b2 being strict MSAlgebra over S holds
( b2 = SingleAlg S iff for i being set st i in the carrier of S holds
the Sorts of b2 . i = {i} );

Lm1:  for S being non empty ManySortedSign holds
( SingleAlg S is non-empty & SingleAlg S is disjoint_valued )
proof
let S be non empty ManySortedSign ; ::_thesis: ( SingleAlg S is non-empty & SingleAlg S is disjoint_valued )
set F = the Sorts of (SingleAlg S);
hereby  :: according to MSUALG_1:def_3,PBOOLE:def_13 ::_thesis: SingleAlg S is disjoint_valued
let x be set ; ::_thesis: ( x in the carrier of S implies not the Sorts of (SingleAlg S) . x is empty )
assume  x in the carrier of S ; ::_thesis: not the Sorts of (SingleAlg S) . x is empty
then  the Sorts of (SingleAlg S) . x = {x} by Def3;
hence  not the Sorts of (SingleAlg S) . x is empty ; ::_thesis: verum
end;
let x, y be set ; :: according to PROB_2:def_2,MSAFREE1:def_2 ::_thesis: ( x = y or the Sorts of (SingleAlg S) . x misses the Sorts of (SingleAlg S) . y )
assume A1: x <> y ; ::_thesis: the Sorts of (SingleAlg S) . x misses the Sorts of (SingleAlg S) . y
percases ( ( x in dom the Sorts of (SingleAlg S) & y in dom the Sorts of (SingleAlg S) ) or not x in dom the Sorts of (SingleAlg S) or not y in dom the Sorts of (SingleAlg S) ) ;
supposeA2: ( x in dom the Sorts of (SingleAlg S) & y in dom the Sorts of (SingleAlg S) ) ; ::_thesis: the Sorts of (SingleAlg S) . x misses the Sorts of (SingleAlg S) . y
 dom the Sorts of (SingleAlg S) = the carrier of S by PARTFUN1:def_2;
then A3: ( the Sorts of (SingleAlg S) . x = {x} & the Sorts of (SingleAlg S) . y = {y} ) by A2, Def3;
assume  the Sorts of (SingleAlg S) . x meets the Sorts of (SingleAlg S) . y ; ::_thesis: contradiction
hence  contradiction by A1, A3, ZFMISC_1:11; ::_thesis: verum
end;
suppose ( not x in dom the Sorts of (SingleAlg S) or not y in dom the Sorts of (SingleAlg S) ) ; ::_thesis: the Sorts of (SingleAlg S) . x misses the Sorts of (SingleAlg S) . y
then  ( the Sorts of (SingleAlg S) . x = {} or the Sorts of (SingleAlg S) . y = {} ) by FUNCT_1:def_2;
hence  the Sorts of (SingleAlg S) . x misses the Sorts of (SingleAlg S) . y by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;

registration
let S be non empty ManySortedSign ;
cluster non-empty disjoint_valued for MSAlgebra over S;
existence
 ex b1 being MSAlgebra over S st
( b1 is non-empty & b1 is disjoint_valued )
proof
 ( SingleAlg S is non-empty & SingleAlg S is disjoint_valued ) by Lm1;
hence  ex b1 being MSAlgebra over S st
( b1 is non-empty & b1 is disjoint_valued ) ; ::_thesis: verum
end;
end;

registration
let S be non empty ManySortedSign ;
cluster SingleAlg S ->  strict non-empty disjoint_valued ;
coherence
 ( SingleAlg S is non-empty & SingleAlg S is disjoint_valued ) by Lm1;
end;

registration
let S be non empty ManySortedSign ;
let A be disjoint_valued MSAlgebra over S;
cluster the Sorts of A ->  disjoint_valued ;
coherence
 the Sorts of A is disjoint_valued by Def2;
end;

theorem Th5: :: MSAFREE1:5
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A1 being non-empty disjoint_valued MSAlgebra over S
for A2 being non-empty MSAlgebra over S
for f being ManySortedFunction of A1,A2
for a being Element of Args (o,A1) holds (Flatten f) * a = f # a
proof
let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S
for A1 being non-empty disjoint_valued MSAlgebra over S
for A2 being non-empty MSAlgebra over S
for f being ManySortedFunction of A1,A2
for a being Element of Args (o,A1) holds (Flatten f) * a = f # a
let o be OperSymbol of S; ::_thesis: for A1 being non-empty disjoint_valued MSAlgebra over S
for A2 being non-empty MSAlgebra over S
for f being ManySortedFunction of A1,A2
for a being Element of Args (o,A1) holds (Flatten f) * a = f # a
let A1 be non-empty disjoint_valued MSAlgebra over S; ::_thesis: for A2 being non-empty MSAlgebra over S
for f being ManySortedFunction of A1,A2
for a being Element of Args (o,A1) holds (Flatten f) * a = f # a
let A2 be non-empty MSAlgebra over S; ::_thesis: for f being ManySortedFunction of A1,A2
for a being Element of Args (o,A1) holds (Flatten f) * a = f # a
let f be ManySortedFunction of A1,A2; ::_thesis: for a being Element of Args (o,A1) holds (Flatten f) * a = f # a
let a be Element of Args (o,A1); ::_thesis: (Flatten f) * a = f # a
A1: dom the Arity of S = the carrier' of S by FUNCT_2:def_1;
set s = the_arity_of o;
 a in (( the Sorts of A1 #) * the Arity of S) . o ;
then  a in ( the Sorts of A1 #) . ( the Arity of S . o) by A1, FUNCT_1:13;
then A2: a in product ( the Sorts of A1 * (the_arity_of o)) by FINSEQ_2:def_5;
then  rng a c= Union ( the Sorts of A1 * (the_arity_of o)) by Th1;
then  ( union (rng ( the Sorts of A1 * (the_arity_of o))) c= union (rng the Sorts of A1) & rng a c= union (rng ( the Sorts of A1 * (the_arity_of o))) ) by CARD_3:def_4, RELAT_1:26, ZFMISC_1:77;
then  rng a c= union (rng the Sorts of A1) by XBOOLE_1:1;
then  rng a c= Union the Sorts of A1 by CARD_3:def_4;
then  rng a c= dom (Flatten f) by FUNCT_2:def_1;
then A3: dom ((Flatten f) * a) = dom a by RELAT_1:27;
A4: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4;
 dom the Sorts of A1 = the carrier of S by PARTFUN1:def_2;
then A5: dom ( the Sorts of A1 * (the_arity_of o)) = dom (the_arity_of o) by A4, RELAT_1:27;
A6: dom a = dom ( the Sorts of A1 * (the_arity_of o)) by A2, CARD_3:9;
A7: now__::_thesis:_for_x_being_set_st_x_in_dom_(_the_Sorts_of_A2_*_(the_arity_of_o))_holds_
((Flatten_f)_*_a)_._x_in_(_the_Sorts_of_A2_*_(the_arity_of_o))_._x
let x be set ; ::_thesis: ( x in dom ( the Sorts of A2 * (the_arity_of o)) implies ((Flatten f) * a) . x in ( the Sorts of A2 * (the_arity_of o)) . x )
assume A8: x in dom ( the Sorts of A2 * (the_arity_of o)) ; ::_thesis: ((Flatten f) * a) . x in ( the Sorts of A2 * (the_arity_of o)) . x
A9: dom ( the Sorts of A2 * (the_arity_of o)) c= dom (the_arity_of o) by RELAT_1:25;
then A10: the Sorts of A2 . ((the_arity_of o) . x) = ( the Sorts of A2 * (the_arity_of o)) . x by A8, FUNCT_1:13;
 (the_arity_of o) . x in rng (the_arity_of o) by A9, A8, FUNCT_1:def_3;
then reconsider z = (the_arity_of o) . x as SortSymbol of S by A4;
 the Sorts of A1 . ((the_arity_of o) . x) = ( the Sorts of A1 * (the_arity_of o)) . x by A9, A8, FUNCT_1:13;
then A11: a . x in the Sorts of A1 . z by A2, A5, A9, A8, CARD_3:9;
((Flatten f) * a) . x = (Flatten f) . (a . x) by A6, A5, A9, A8, FUNCT_1:13
.= (f . z) . (a . x) by A11, Def1 ;
hence  ((Flatten f) * a) . x in ( the Sorts of A2 * (the_arity_of o)) . x by A10, A11, FUNCT_2:5; ::_thesis: verum
end;
 dom the Sorts of A2 = the carrier of S by PARTFUN1:def_2;
then  dom (the_arity_of o) = dom ( the Sorts of A2 * (the_arity_of o)) by A4, RELAT_1:27;
then  (Flatten f) * a in product ( the Sorts of A2 * (the_arity_of o)) by A3, A6, A5, A7, CARD_3:9;
then  (Flatten f) * a in ( the Sorts of A2 #) . ( the Arity of S . o) by FINSEQ_2:def_5;
then reconsider x = (Flatten f) * a as Element of Args (o,A2) by A1, FUNCT_1:13;
now__::_thesis:_for_n_being_Nat_st_n_in_dom_a_holds_
x_._n_=_(f_._((the_arity_of_o)_/._n))_._(a_._n)
let n be Nat; ::_thesis: ( n in dom a implies x . n = (f . ((the_arity_of o) /. n)) . (a . n) )
assume A12: n in dom a ; ::_thesis: x . n = (f . ((the_arity_of o) /. n)) . (a . n)
then  ( (the_arity_of o) /. n = (the_arity_of o) . n & a . n in ( the Sorts of A1 * (the_arity_of o)) . n ) by A2, A6, A5, CARD_3:9, PARTFUN1:def_6;
then A13: a . n in the Sorts of A1 . ((the_arity_of o) /. n) by A6, A5, A12, FUNCT_1:13;
thus x . n = (Flatten f) . (a . n) by A12, FUNCT_1:13
.= (f . ((the_arity_of o) /. n)) . (a . n) by A13, Def1 ; ::_thesis: verum
end;
hence  (Flatten f) * a = f # a by MSUALG_3:def_6; ::_thesis: verum
end;

registration
let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of the carrier of S;
cluster FreeSort X ->  disjoint_valued ;
coherence
 FreeSort X is disjoint_valued
proof
let x, y be set ; :: according to PROB_2:def_2 ::_thesis: ( x = y or (FreeSort X) . x misses (FreeSort X) . y )
set F = FreeSort X;
percases ( ( x in dom (FreeSort X) & y in dom (FreeSort X) ) or not x in dom (FreeSort X) or not y in dom (FreeSort X) ) ;
suppose ( x in dom (FreeSort X) & y in dom (FreeSort X) ) ; ::_thesis: ( x = y or (FreeSort X) . x misses (FreeSort X) . y )
then reconsider s1 = x, s2 = y as SortSymbol of S by PARTFUN1:def_2;
assume  x <> y ; ::_thesis: (FreeSort X) . x misses (FreeSort X) . y
then  (FreeSort X) . s1 misses (FreeSort X) . s2 by MSAFREE:12;
hence  (FreeSort X) . x misses (FreeSort X) . y ; ::_thesis: verum
end;
supposeA1: ( not x in dom (FreeSort X) or not y in dom (FreeSort X) ) ; ::_thesis: ( x = y or (FreeSort X) . x misses (FreeSort X) . y )
assume  x <> y ; ::_thesis: (FreeSort X) . x misses (FreeSort X) . y
 ( (FreeSort X) . x = {} or (FreeSort X) . y = {} ) by A1, FUNCT_1:def_2;
hence  (FreeSort X) . x misses (FreeSort X) . y by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
end;

scheme :: MSAFREE1:sch 2
FreeSortUniq{ F1() ->  non empty non void ManySortedSign , F2() ->  V2() ManySortedSet of the carrier of F1(), F3() ->  V2() ManySortedSet of the carrier of F1(), F4( set ) ->  Element of Union F3(), F5( set , set , set ) ->  Element of Union F3(), F6() ->  ManySortedFunction of FreeSort F2(),F3(), F7() ->  ManySortedFunction of FreeSort F2(),F3() } :
 F6() = F7()
provided
A1: for o being OperSymbol of F1()
for ts being Element of Args (o,(FreeMSA F2()))
for x being Element of (Union F3()) * st x = (Flatten F6()) * ts holds
(F6() . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = F5(o,ts,x) and
A2: for s being SortSymbol of F1()
for y being set st y in FreeGen (s,F2()) holds
(F6() . s) . y = F4(y) and
A3: for o being OperSymbol of F1()
for ts being Element of Args (o,(FreeMSA F2()))
for x being Element of (Union F3()) * st x = (Flatten F7()) * ts holds
(F7() . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = F5(o,ts,x) and
A4: for s being SortSymbol of F1()
for y being set st y in FreeGen (s,F2()) holds
(F7() . s) . y = F4(y)
proof
reconsider D = Union F3() as non empty set ;
TS (DTConMSA F2()) = union (rng (FreeSort F2())) by MSAFREE:11
.= Union (FreeSort F2()) by CARD_3:def_4 ;
then reconsider f1 = Flatten F6(), f2 = Flatten F7() as Function of (TS (DTConMSA F2())),D ;
deffunc H1( Element of (DTConMSA F2()), Element of (TS (DTConMSA F2())) * , Element of (Union F3()) * ) ->  Element of Union F3() = F5(($1 `1),$2,$3);
consider H being Function of [: the carrier of (DTConMSA F2()),((TS (DTConMSA F2())) *),((Union F3()) *):],(Union F3()) such that
A5: for nt being Element of (DTConMSA F2())
for ts being Element of (TS (DTConMSA F2())) *
for x being Element of (Union F3()) * holds H . (nt,ts,x) = H1(nt,ts,x) from MULTOP_1:sch_4();
reconsider H = H as Function of [: the carrier of (DTConMSA F2()),((TS (DTConMSA F2())) *),(D *):],D ;
deffunc H2( Element of (DTConMSA F2()), Element of (TS (DTConMSA F2())) * , Element of D * ) ->  Element of D = H . ($1,$2,$3);
A6: DTConMSA F2() = DTConstrStr(# ([: the carrier' of F1(),{ the carrier of F1()}:] \/ (Union (coprod F2()))),(REL F2()) #) by MSAFREE:def_8;
A7: now__::_thesis:_for_f_being_ManySortedFunction_of_FreeSort_F2(),F3()_st_(_for_o_being_OperSymbol_of_F1()
for_ts_being_Element_of_Args_(o,(FreeMSA_F2()))
for_x_being_Element_of_D_*_st_x_=_(Flatten_f)_*_ts_holds_
(f_._(the_result_sort_of_o))_._((Den_(o,(FreeMSA_F2())))_._ts)_=_F5(o,ts,x)_)_holds_
for_nt_being_Element_of_(DTConMSA_F2())
for_ts_being_Element_of_(TS_(DTConMSA_F2()))_*_st_nt_==>_roots_ts_holds_
for_x_being_Element_of_D_*_st_x_=_(Flatten_f)_*_ts_holds_
(Flatten_f)_._(nt_-tree_ts)_=_H_._(nt,ts,x)
let f be ManySortedFunction of FreeSort F2(),F3(); ::_thesis: ( ( for o being OperSymbol of F1()
for ts being Element of Args (o,(FreeMSA F2()))
for x being Element of D * st x = (Flatten f) * ts holds
(f . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = F5(o,ts,x) ) implies for nt being Element of (DTConMSA F2())
for ts being Element of (TS (DTConMSA F2())) * st nt ==> roots ts holds
for x being Element of D * st x = (Flatten f) * ts holds
(Flatten f) . (nt -tree ts) = H . (nt,ts,x) )
assume A8: for o being OperSymbol of F1()
for ts being Element of Args (o,(FreeMSA F2()))
for x being Element of D * st x = (Flatten f) * ts holds
(f . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = F5(o,ts,x) ; ::_thesis: for nt being Element of (DTConMSA F2())
for ts being Element of (TS (DTConMSA F2())) * st nt ==> roots ts holds
for x being Element of D * st x = (Flatten f) * ts holds
(Flatten f) . (nt -tree ts) = H . (nt,ts,x)
let nt be Element of (DTConMSA F2()); ::_thesis: for ts being Element of (TS (DTConMSA F2())) * st nt ==> roots ts holds
for x being Element of D * st x = (Flatten f) * ts holds
(Flatten f) . (nt -tree ts) = H . (nt,ts,x)
let ts be Element of (TS (DTConMSA F2())) * ; ::_thesis: ( nt ==> roots ts implies for x being Element of D * st x = (Flatten f) * ts holds
(Flatten f) . (nt -tree ts) = H . (nt,ts,x) )
assume A9: nt ==> roots ts ; ::_thesis: for x being Element of D * st x = (Flatten f) * ts holds
(Flatten f) . (nt -tree ts) = H . (nt,ts,x)
then  [nt,(roots ts)] in REL F2() by A6, LANG1:def_1;
then consider o being OperSymbol of F1(), x2 being Element of { the carrier of F1()} such that
A10: nt = [o,x2] by Th2, DOMAIN_1:1;
let x be Element of D * ; ::_thesis: ( x = (Flatten f) * ts implies (Flatten f) . (nt -tree ts) = H . (nt,ts,x) )
assume A11: x = (Flatten f) * ts ; ::_thesis: (Flatten f) . (nt -tree ts) = H . (nt,ts,x)
A12: FreeMSA F2() = MSAlgebra(# (FreeSort F2()),(FreeOper F2()) #) by MSAFREE:def_14;
reconsider tss = ts as FinSequence of TS (DTConMSA F2()) by FINSEQ_1:def_11;
reconsider xx = x as Element of (Union F3()) * ;
A13: x2 = the carrier of F1() by TARSKI:def_1;
then A14: nt = Sym (o,F2()) by A10, MSAFREE:def_9;
then A15: tss in (((FreeSort F2()) #) * the Arity of F1()) . o by A9, MSAFREE:10;
 ((FreeSort F2()) * the ResultSort of F1()) . o = (FreeSort F2()) . (the_result_sort_of o) by FUNCT_2:15;
then A16: (DenOp (o,F2())) . ts in (FreeSort F2()) . (the_result_sort_of o) by A15, FUNCT_2:5;
(Flatten f) . ([o, the carrier of F1()] -tree ts) = (Flatten f) . ((DenOp (o,F2())) . tss) by A9, A10, A13, A14, MSAFREE:def_12
.= (f . (the_result_sort_of o)) . ((DenOp (o,F2())) . ts) by A16, Def1
.= (f . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) by A12, MSAFREE:def_13
.= F5(o,ts,x) by A8, A12, A15, A11
.= F5((nt `1),ts,x) by A10, MCART_1:7 ;
hence (Flatten f) . (nt -tree ts) = H1(nt,ts,xx) by A10, A13
.= H . (nt,ts,x) by A5 ;
::_thesis: verum
end;
then A17: for nt being Symbol of (DTConMSA F2())
for ts being Element of (TS (DTConMSA F2())) * st nt ==> roots ts holds
for x being Element of D * st x = f1 * ts holds
f1 . (nt -tree ts) = H2(nt,ts,x) by A1;
deffunc H3( Element of (DTConMSA F2())) ->  Element of Union F3() = F4((root-tree $1));
A18: Terminals (DTConMSA F2()) = Union (coprod F2()) by MSAFREE:6;
consider G being Function of the carrier of (DTConMSA F2()),(Union F3()) such that
A19: for t being Element of (DTConMSA F2()) holds G . t = H3(t) from FUNCT_2:sch_4();
reconsider G = G as Function of the carrier of (DTConMSA F2()),D ;
deffunc H4( Element of (DTConMSA F2())) ->  Element of D = G . $1;
A20: dom F2() = the carrier of F1() by PARTFUN1:def_2;
A21: now__::_thesis:_for_f_being_ManySortedFunction_of_FreeSort_F2(),F3()_st_(_for_s_being_SortSymbol_of_F1()
for_y_being_set_st_y_in_FreeGen_(s,F2())_holds_
(f_._s)_._y_=_F4(y)_)_holds_
for_t_being_Element_of_(DTConMSA_F2())_st_t_in_Terminals_(DTConMSA_F2())_holds_
(Flatten_f)_._(root-tree_t)_=_G_._t
let f be ManySortedFunction of FreeSort F2(),F3(); ::_thesis: ( ( for s being SortSymbol of F1()
for y being set st y in FreeGen (s,F2()) holds
(f . s) . y = F4(y) ) implies for t being Element of (DTConMSA F2()) st t in Terminals (DTConMSA F2()) holds
(Flatten f) . (root-tree t) = G . t )
assume A22: for s being SortSymbol of F1()
for y being set st y in FreeGen (s,F2()) holds
(f . s) . y = F4(y) ; ::_thesis: for t being Element of (DTConMSA F2()) st t in Terminals (DTConMSA F2()) holds
(Flatten f) . (root-tree t) = G . t
let t be Element of (DTConMSA F2()); ::_thesis: ( t in Terminals (DTConMSA F2()) implies (Flatten f) . (root-tree t) = G . t )
assume A23: t in Terminals (DTConMSA F2()) ; ::_thesis: (Flatten f) . (root-tree t) = G . t
then reconsider s = t `2 as SortSymbol of F1() by A18, A20, CARD_3:22;
 t `1 in F2() . (t `2) by A18, A23, CARD_3:22;
then A24: root-tree [(t `1),s] in FreeGen (s,F2()) by MSAFREE:def_15;
A25: t = [(t `1),(t `2)] by A18, A23, CARD_3:22;
hence (Flatten f) . (root-tree t) = (f . s) . (root-tree [(t `1),s]) by A24, Def1
.= F4((root-tree t)) by A22, A25, A24
.= G . t by A19 ;
::_thesis: verum
end;
then A26: for t being Symbol of (DTConMSA F2()) st t in Terminals (DTConMSA F2()) holds
f2 . (root-tree t) = H4(t) by A4;
A27: for nt being Symbol of (DTConMSA F2())
for ts being Element of (TS (DTConMSA F2())) * st nt ==> roots ts holds
for x being Element of D * st x = f2 * ts holds
f2 . (nt -tree ts) = H2(nt,ts,x) by A3, A7;
A28: for t being Element of (DTConMSA F2()) st t in Terminals (DTConMSA F2()) holds
f1 . (root-tree t) = H4(t) by A2, A21;
 f1 = f2 from MSAFREE1:sch_1(A28, A17, A26, A27);
hence  F6() = F7() by Th4; ::_thesis: verum
end;

registration
let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of the carrier of S;
cluster FreeMSA X ->  non-empty ;
coherence
 FreeMSA X is non-empty ;
end;

registration
let S be non empty non void ManySortedSign ;
let o be OperSymbol of S;
let A be non-empty MSAlgebra over S;
cluster Args (o,A) ->  non empty ;
coherence
 not Args (o,A) is empty ;
cluster Result (o,A) ->  non empty ;
coherence
 not Result (o,A) is empty ;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of the carrier of S;
cluster the Sorts of (FreeMSA X) ->  disjoint_valued ;
coherence
 the Sorts of (FreeMSA X) is disjoint_valued
proof
 FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def_14;
hence  the Sorts of (FreeMSA X) is disjoint_valued ; ::_thesis: verum
end;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of the carrier of S;
cluster FreeMSA X ->  disjoint_valued ;
coherence
 FreeMSA X is disjoint_valued
proof
thus  the Sorts of (FreeMSA X) is disjoint_valued ; :: according to MSAFREE1:def_2 ::_thesis: verum
end;
end;

scheme :: MSAFREE1:sch 3
ExtFreeGen{ F1() ->  non empty non void ManySortedSign , F2() ->  V2() ManySortedSet of the carrier of F1(), F3() ->  non-empty MSAlgebra over F1(), P1[ set , set , set ], F4() ->  ManySortedFunction of (FreeMSA F2()),F3(), F5() ->  ManySortedFunction of (FreeMSA F2()),F3() } :
 F4() = F5()
provided
A1: F4() is_homomorphism FreeMSA F2(),F3() and
A2: for s being SortSymbol of F1()
for x, y being set st y in FreeGen (s,F2()) holds
( (F4() . s) . y = x iff P1[s,x,y] ) and
A3: F5() is_homomorphism FreeMSA F2(),F3() and
A4: for s being SortSymbol of F1()
for x, y being set st y in FreeGen (s,F2()) holds
( (F5() . s) . y = x iff P1[s,x,y] )
proof
defpred S1[ set , set ] means  for s being SortSymbol of F1() st $1 in FreeGen (s,F2()) holds
P1[s,$2,$1];
A5: FreeMSA F2() = MSAlgebra(# (FreeSort F2()),(FreeOper F2()) #) by MSAFREE:def_14;
then reconsider f1 = F4(), f2 = F5() as ManySortedFunction of FreeSort F2(), the Sorts of F3() ;
A6: for x being set st x in Union (FreeGen F2()) holds
ex y being set st
( y in Union the Sorts of F3() & S1[x,y] )
proof
let e be set ; ::_thesis: ( e in Union (FreeGen F2()) implies ex y being set st
( y in Union the Sorts of F3() & S1[e,y] ) )
A7: dom the Sorts of F3() = the carrier of F1() by PARTFUN1:def_2;
assume  e in Union (FreeGen F2()) ; ::_thesis: ex y being set st
( y in Union the Sorts of F3() & S1[e,y] )
then consider s being set  such that
A8: s in dom (FreeGen F2()) and
A9: e in (FreeGen F2()) . s by CARD_5:2;
reconsider s = s as SortSymbol of F1() by A8, PARTFUN1:def_2;
A10: e in FreeGen (s,F2()) by A9, MSAFREE:def_16;
take u = (F4() . s) . e; ::_thesis: ( u in Union the Sorts of F3() & S1[e,u] )
 f1 . s is Function of ((FreeSort F2()) . s),( the Sorts of F3() . s) ;
then  u in the Sorts of F3() . s by A10, FUNCT_2:5;
hence  u in Union the Sorts of F3() by A7, CARD_5:2; ::_thesis: S1[e,u]
let s9 be SortSymbol of F1(); ::_thesis: ( e in FreeGen (s9,F2()) implies P1[s9,u,e] )
assume A11: e in FreeGen (s9,F2()) ; ::_thesis: P1[s9,u,e]
then  ((FreeSort F2()) . s9) /\ ((FreeSort F2()) . s) <> {} by A10, XBOOLE_0:def_4;
then  (FreeSort F2()) . s9 meets (FreeSort F2()) . s by XBOOLE_0:def_7;
then  s = s9 by MSAFREE:12;
hence  P1[s9,u,e] by A2, A11; ::_thesis: verum
end;
consider G being Function of (Union (FreeGen F2())),(Union the Sorts of F3()) such that
A12: for e being set st e in Union (FreeGen F2()) holds
S1[e,G . e] from FUNCT_2:sch_1(A6);
deffunc H1( set ) ->  Element of Union the Sorts of F3() = G /. $1;
defpred S2[ set , set ] means  for o being OperSymbol of F1()
for a being Element of Args (o,F3()) st $1 = [o,a] holds
$2 = (Den (o,F3())) . a;
consider R being set  such that
A13: R =  {  [o,a] where o is Element of the carrier' of F1(), a is Element of Args (o,F3()) : verum  }  ;
A14: for s being SortSymbol of F1()
for y being set st y in FreeGen (s,F2()) holds
(f1 . s) . y = H1(y)
proof
let s be SortSymbol of F1(); ::_thesis: for y being set st y in FreeGen (s,F2()) holds
(f1 . s) . y = H1(y)
let y be set ; ::_thesis: ( y in FreeGen (s,F2()) implies (f1 . s) . y = H1(y) )
A15: dom (FreeGen F2()) = the carrier of F1() by PARTFUN1:def_2;
assume A16: y in FreeGen (s,F2()) ; ::_thesis: (f1 . s) . y = H1(y)
then  y in (FreeGen F2()) . s by MSAFREE:def_16;
then A17: y in Union (FreeGen F2()) by A15, CARD_5:2;
then  P1[s,G . y,y] by A12, A16;
hence (f1 . s) . y = G . y by A2, A16
.= G /. y by A17, FUNCT_2:def_13 ;
::_thesis: verum
end;
A18: for x being set st x in R holds
ex y being set st
( y in Union the Sorts of F3() & S2[x,y] )
proof
let e be set ; ::_thesis: ( e in R implies ex y being set st
( y in Union the Sorts of F3() & S2[e,y] ) )
assume  e in R ; ::_thesis: ex y being set st
( y in Union the Sorts of F3() & S2[e,y] )
then consider o being OperSymbol of F1(), a being Element of Args (o,F3()) such that
A19: e = [o,a] by A13;
reconsider u = (Den (o,F3())) . a as set ;
take  u ; ::_thesis: ( u in Union the Sorts of F3() & S2[e,u] )
 u in union (rng the Sorts of F3()) by TARSKI:def_4;
hence  u in Union the Sorts of F3() by CARD_3:def_4; ::_thesis: S2[e,u]
let o9 be OperSymbol of F1(); ::_thesis: for a being Element of Args (o9,F3()) st e = [o9,a] holds
u = (Den (o9,F3())) . a
let x9 be Element of Args (o9,F3()); ::_thesis: ( e = [o9,x9] implies u = (Den (o9,F3())) . x9 )
assume A20: e = [o9,x9] ; ::_thesis: u = (Den (o9,F3())) . x9
then  o = o9 by A19, XTUPLE_0:1;
hence  u = (Den (o9,F3())) . x9 by A19, A20, XTUPLE_0:1; ::_thesis: verum
end;
consider H being Function of R,(Union the Sorts of F3()) such that
A21: for e being set st e in R holds
S2[e,H . e] from FUNCT_2:sch_1(A18);
A22: for s being SortSymbol of F1()
for y being set st y in FreeGen (s,F2()) holds
(f2 . s) . y = H1(y)
proof
let s be SortSymbol of F1(); ::_thesis: for y being set st y in FreeGen (s,F2()) holds
(f2 . s) . y = H1(y)
let y be set ; ::_thesis: ( y in FreeGen (s,F2()) implies (f2 . s) . y = H1(y) )
A23: dom (FreeGen F2()) = the carrier of F1() by PARTFUN1:def_2;
assume A24: y in FreeGen (s,F2()) ; ::_thesis: (f2 . s) . y = H1(y)
then  y in (FreeGen F2()) . s by MSAFREE:def_16;
then A25: y in Union (FreeGen F2()) by A23, CARD_5:2;
then  P1[s,G . y,y] by A12, A24;
hence (f2 . s) . y = G . y by A4, A24
.= G /. y by A25, FUNCT_2:def_13 ;
::_thesis: verum
end;
deffunc H2( set , set , set ) ->  Element of Union the Sorts of F3() = H /. [$1,$3];
A26: for o being OperSymbol of F1()
for ts being Element of Args (o,(FreeMSA F2()))
for x being Element of (Union the Sorts of F3()) * st x = (Flatten f2) * ts holds
(f2 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x)
proof
let o be OperSymbol of F1(); ::_thesis: for ts being Element of Args (o,(FreeMSA F2()))
for x being Element of (Union the Sorts of F3()) * st x = (Flatten f2) * ts holds
(f2 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x)
let ts be Element of Args (o,(FreeMSA F2())); ::_thesis: for x being Element of (Union the Sorts of F3()) * st x = (Flatten f2) * ts holds
(f2 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x)
let x be Element of (Union the Sorts of F3()) * ; ::_thesis: ( x = (Flatten f2) * ts implies (f2 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x) )
assume A27: x = (Flatten f2) * ts ; ::_thesis: (f2 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x)
A28: (Flatten f2) * ts = F5() # ts by A5, Th5;
then reconsider a = x as Element of Args (o,F3()) by A27;
A29: [o,a] in R by A13;
thus (f2 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = (Den (o,F3())) . a by A3, A28, A27, MSUALG_3:def_7
.= H . [o,x] by A21, A29
.= H /. [o,x] by A29, FUNCT_2:def_13 ; ::_thesis: verum
end;
A30: for o being OperSymbol of F1()
for ts being Element of Args (o,(FreeMSA F2()))
for x being Element of (Union the Sorts of F3()) * st x = (Flatten f1) * ts holds
(f1 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x)
proof
let o be OperSymbol of F1(); ::_thesis: for ts being Element of Args (o,(FreeMSA F2()))
for x being Element of (Union the Sorts of F3()) * st x = (Flatten f1) * ts holds
(f1 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x)
let ts be Element of Args (o,(FreeMSA F2())); ::_thesis: for x being Element of (Union the Sorts of F3()) * st x = (Flatten f1) * ts holds
(f1 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x)
let x be Element of (Union the Sorts of F3()) * ; ::_thesis: ( x = (Flatten f1) * ts implies (f1 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x) )
assume A31: x = (Flatten f1) * ts ; ::_thesis: (f1 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x)
A32: (Flatten f1) * ts = F4() # ts by A5, Th5;
then reconsider a = x as Element of Args (o,F3()) by A31;
A33: [o,a] in R by A13;
thus (f1 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = (Den (o,F3())) . a by A1, A32, A31, MSUALG_3:def_7
.= H . [o,x] by A21, A33
.= H /. [o,x] by A33, FUNCT_2:def_13 ; ::_thesis: verum
end;
 f1 = f2 from MSAFREE1:sch_2(A30, A14, A26, A22);
hence  F4() = F5() ; ::_thesis: verum
end;