let S be non empty non void ManySortedSign ; :: thesis: for X being V2() ManySortedSet of the carrier of S holds hom ((id the carrier of S),(id the carrier' of S),X,S,S) = id the Sorts of (FreeMSA X)

let X be V2() ManySortedSet of the carrier of S; :: thesis: hom ((id the carrier of S),(id the carrier' of S),X,S,S) = id the Sorts of (FreeMSA X)

set f = id the carrier of S;

set h = hom ((id the carrier of S),(id the carrier' of S),X,S,S);

set I = id the Sorts of (FreeMSA X);

set g = id the carrier' of S;

A1: id the carrier of S, id the carrier' of S form_morphism_between S,S by PUA2MSS1:28;

dom X = the carrier of S by PARTFUN1:def 2;

then A2: X * (id the carrier of S) = X by RELAT_1:52;

A3: (FreeMSA X) | (S,(id the carrier of S),(id the carrier' of S)) = FreeMSA X by Th25;

hence hom ((id the carrier of S),(id the carrier' of S),X,S,S) = id the Sorts of (FreeMSA X) by A2, A3, A4, EXTENS_1:19, PBOOLE:3; :: thesis: verum

let X be V2() ManySortedSet of the carrier of S; :: thesis: hom ((id the carrier of S),(id the carrier' of S),X,S,S) = id the Sorts of (FreeMSA X)

set f = id the carrier of S;

set h = hom ((id the carrier of S),(id the carrier' of S),X,S,S);

set I = id the Sorts of (FreeMSA X);

set g = id the carrier' of S;

A1: id the carrier of S, id the carrier' of S form_morphism_between S,S by PUA2MSS1:28;

dom X = the carrier of S by PARTFUN1:def 2;

then A2: X * (id the carrier of S) = X by RELAT_1:52;

A3: (FreeMSA X) | (S,(id the carrier of S),(id the carrier' of S)) = FreeMSA X by Th25;

A4: now :: thesis: for i being object st i in the carrier of S holds

((id the Sorts of (FreeMSA X)) || (FreeGen X)) . i = ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) || (FreeGen (X * (id the carrier of S)))) . i

( id the Sorts of (FreeMSA X) is_homomorphism FreeMSA X, FreeMSA X & hom ((id the carrier of S),(id the carrier' of S),X,S,S) is_homomorphism FreeMSA (X * (id the carrier of S)),(FreeMSA X) | (S,(id the carrier of S),(id the carrier' of S)) )
by A1, Def5, MSUALG_3:9;((id the Sorts of (FreeMSA X)) || (FreeGen X)) . i = ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) || (FreeGen (X * (id the carrier of S)))) . i

let i be object ; :: thesis: ( i in the carrier of S implies ((id the Sorts of (FreeMSA X)) || (FreeGen X)) . i = ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) || (FreeGen (X * (id the carrier of S)))) . i )

assume i in the carrier of S ; :: thesis: ((id the Sorts of (FreeMSA X)) || (FreeGen X)) . i = ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) || (FreeGen (X * (id the carrier of S)))) . i

then reconsider s = i as SortSymbol of S ;

FreeGen X c= the Sorts of (FreeMSA X) by PBOOLE:def 18;

then A5: (FreeGen X) . s c= the Sorts of (FreeMSA X) . s ;

then ((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s) is Function of ((FreeGen X) . s),( the Sorts of (FreeMSA X) . s) by FUNCT_2:32;

then A6: dom (((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) = (FreeGen X) . s by FUNCT_2:def 1;

then A11: dom (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s)) = (FreeGen X) . s by FUNCT_2:def 1;

( ((id the Sorts of (FreeMSA X)) || (FreeGen X)) . s = ((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s) & ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) || (FreeGen (X * (id the carrier of S)))) . s = ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen (X * (id the carrier of S))) . s) ) by MSAFREE:def 1;

hence ((id the Sorts of (FreeMSA X)) || (FreeGen X)) . i = ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) || (FreeGen (X * (id the carrier of S)))) . i by A2, A6, A11, A7; :: thesis: verum

end;assume i in the carrier of S ; :: thesis: ((id the Sorts of (FreeMSA X)) || (FreeGen X)) . i = ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) || (FreeGen (X * (id the carrier of S)))) . i

then reconsider s = i as SortSymbol of S ;

FreeGen X c= the Sorts of (FreeMSA X) by PBOOLE:def 18;

then A5: (FreeGen X) . s c= the Sorts of (FreeMSA X) . s ;

then ((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s) is Function of ((FreeGen X) . s),( the Sorts of (FreeMSA X) . s) by FUNCT_2:32;

then A6: dom (((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) = (FreeGen X) . s by FUNCT_2:def 1;

A7: now :: thesis: for a being object st a in (FreeGen X) . s holds

(((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) . a = (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s)) . a

((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s) is Function of ((FreeGen X) . s),( the Sorts of (FreeMSA X) . s)
by A2, A3, A5, FUNCT_2:32;(((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) . a = (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s)) . a

let a be object ; :: thesis: ( a in (FreeGen X) . s implies (((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) . a = (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s)) . a )

assume A8: a in (FreeGen X) . s ; :: thesis: (((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) . a = (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s)) . a

then reconsider b = a as Element of (FreeMSA X),s by A5;

b in FreeGen (s,X) by A8, MSAFREE:def 16;

then consider x being set such that

A9: x in X . s and

A10: b = root-tree [x,s] by MSAFREE:def 15;

thus (((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) . a = ((id the Sorts of (FreeMSA X)) . s) . b by A8, FUNCT_1:49

.= (id ( the Sorts of (FreeMSA X) . s)) . b by MSUALG_3:def 1

.= b

.= root-tree [x,((id the carrier of S) . s)] by A10

.= ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) . b by A1, A2, A9, A10, Def5

.= (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s)) . a by A8, FUNCT_1:49 ; :: thesis: verum

end;assume A8: a in (FreeGen X) . s ; :: thesis: (((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) . a = (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s)) . a

then reconsider b = a as Element of (FreeMSA X),s by A5;

b in FreeGen (s,X) by A8, MSAFREE:def 16;

then consider x being set such that

A9: x in X . s and

A10: b = root-tree [x,s] by MSAFREE:def 15;

thus (((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) . a = ((id the Sorts of (FreeMSA X)) . s) . b by A8, FUNCT_1:49

.= (id ( the Sorts of (FreeMSA X) . s)) . b by MSUALG_3:def 1

.= b

.= root-tree [x,((id the carrier of S) . s)] by A10

.= ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) . b by A1, A2, A9, A10, Def5

.= (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s)) . a by A8, FUNCT_1:49 ; :: thesis: verum

then A11: dom (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s)) = (FreeGen X) . s by FUNCT_2:def 1;

( ((id the Sorts of (FreeMSA X)) || (FreeGen X)) . s = ((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s) & ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) || (FreeGen (X * (id the carrier of S)))) . s = ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen (X * (id the carrier of S))) . s) ) by MSAFREE:def 1;

hence ((id the Sorts of (FreeMSA X)) || (FreeGen X)) . i = ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) || (FreeGen (X * (id the carrier of S)))) . i by A2, A6, A11, A7; :: thesis: verum

hence hom ((id the carrier of S),(id the carrier' of S),X,S,S) = id the Sorts of (FreeMSA X) by A2, A3, A4, EXTENS_1:19, PBOOLE:3; :: thesis: verum