let S be non empty non void ManySortedSign ; 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; 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 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)))) . ilet i be
object ;
( 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
;
((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)))) . ithen 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 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)) . alet a be
object ;
( 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
;
(((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)) . athen 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
;
verum end;
((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;
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;
verum end;
( 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;
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; verum