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 ()
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 ()
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 ();
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 ()) || ()) . 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 ()) || ()) . 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 ()) || ()) . 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 () by PBOOLE:def 18;
then A5: (FreeGen X) . s c= the Sorts of () . s ;
then ((id the Sorts of ()) . s) | (() . s) is Function of (() . s),( the Sorts of () . s) by FUNCT_2:32;
then A6: dom (((id the Sorts of ()) . s) | (() . s)) = () . s by FUNCT_2:def 1;
A7: now :: thesis: for a being object st a in () . s holds
(((id the Sorts of ()) . s) | (() . s)) . a = (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | (() . s)) . a
let a be object ; :: thesis: ( a in () . s implies (((id the Sorts of ()) . s) | (() . s)) . a = (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | (() . s)) . a )
assume A8: a in () . s ; :: thesis: (((id the Sorts of ()) . s) | (() . s)) . a = (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | (() . s)) . a
then reconsider b = a as Element of (),s by A5;
b in FreeGen (s,X) by ;
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 ()) . s) | (() . s)) . a = ((id the Sorts of ()) . s) . b by
.= (id ( the Sorts of () . 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) | (() . s)) . a by ; :: thesis: verum
end;
((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | (() . s) is Function of (() . s),( the Sorts of () . s) by ;
then A11: dom (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | (() . s)) = () . s by FUNCT_2:def 1;
( ((id the Sorts of ()) || ()) . s = ((id the Sorts of ()) . s) | (() . 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 ()) || ()) . 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;
( id the Sorts of () 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)),() | (S,(id the carrier of S),(id the carrier' of S)) ) by ;
hence hom ((id the carrier of S),(id the carrier' of S),X,S,S) = id the Sorts of () by ; :: thesis: verum