defpred S₁[ set , set , set ] means $3 = root-tree [$2,$1];
let IT1, IT2 be ManySortedFunction of (FreeEnv MSA),MSA; :: thesis: ( IT1 is_homomorphism FreeEnv MSA,MSA & ( for s being SortSymbol of S
for x, y being set st y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s holds
(IT1 . s) . y = x ) & IT2 is_homomorphism FreeEnv MSA,MSA & ( for s being SortSymbol of S
for x, y being set st y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s holds
(IT2 . s) . y = x ) implies IT1 = IT2 )
reconsider IT19 = IT1, IT29 = IT2 as ManySortedFunction of (FreeMSA the Sorts of MSA),MSA ;
assume IT1 is_homomorphism FreeEnv MSA,MSA ; :: thesis: ( ex s being SortSymbol of S ex x, y being set st
( y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s & not (IT1 . s) . y = x ) or not IT2 is_homomorphism FreeEnv MSA,MSA or ex s being SortSymbol of S ex x, y being set st
( y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s & not (IT2 . s) . y = x ) or IT1 = IT2 )
then A12: IT19 is_homomorphism FreeMSA the Sorts of MSA,MSA ;
assume A13: for s being SortSymbol of S
for x, y being set st y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s holds
(IT1 . s) . y = x ; :: thesis: ( not IT2 is_homomorphism FreeEnv MSA,MSA or ex s being SortSymbol of S ex x, y being set st
( y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s & not (IT2 . s) . y = x ) or IT1 = IT2 )
A14: for s being SortSymbol of S
for x, y being set st y in FreeGen (s, the Sorts of MSA) holds
( (IT19 . s) . y = x iff S₁[s,x,y] )

proof

let s be SortSymbol of S; :: thesis: for x, y being set st y in FreeGen (s, the Sorts of MSA) holds
( (IT19 . s) . y = x iff S₁[s,x,y] )
let x, y be set ; :: thesis: ( y in FreeGen (s, the Sorts of MSA) implies ( (IT19 . s) . y = x iff S₁[s,x,y] ) )
assume A15: y in FreeGen (s, the Sorts of MSA) ; :: thesis: ( (IT19 . s) . y = x iff S₁[s,x,y] )
then consider a being set such that
A16: a in the Sorts of MSA . s and
A17: y = root-tree [a,s] by MSAFREE:def 15;
y in (FreeSort the Sorts of MSA) . s by A15;
then A18: y in FreeSort ( the Sorts of MSA,s) by MSAFREE:def 11;
hence ( (IT19 . s) . y = x implies y = root-tree [x,s] ) by A13, A16, A17; :: thesis: ( S₁[s,x,y] implies (IT19 . s) . y = x )
assume y = root-tree [x,s] ; :: thesis: (IT19 . s) . y = x
then [x,s] = [a,s] by A17, TREES_4:4;
then x = a by ZFMISC_1:27;
hence (IT19 . s) . y = x by A13, A18, A16, A17; :: thesis: verum

end;

assume IT2 is_homomorphism FreeEnv MSA,MSA ; :: thesis: ( ex s being SortSymbol of S ex x, y being set st
( y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s & not (IT2 . s) . y = x ) or IT1 = IT2 )
then A19: IT29 is_homomorphism FreeMSA the Sorts of MSA,MSA ;
assume A20: for s being SortSymbol of S
for x, y being set st y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s holds
(IT2 . s) . y = x ; :: thesis: IT1 = IT2
A21: for s being SortSymbol of S
for x, y being set st y in FreeGen (s, the Sorts of MSA) holds
( (IT29 . s) . y = x iff S₁[s,x,y] )

proof

let s be SortSymbol of S; :: thesis: for x, y being set st y in FreeGen (s, the Sorts of MSA) holds
( (IT29 . s) . y = x iff S₁[s,x,y] )
let x, y be set ; :: thesis: ( y in FreeGen (s, the Sorts of MSA) implies ( (IT29 . s) . y = x iff S₁[s,x,y] ) )
assume A22: y in FreeGen (s, the Sorts of MSA) ; :: thesis: ( (IT29 . s) . y = x iff S₁[s,x,y] )
then consider a being set such that
A23: a in the Sorts of MSA . s and
A24: y = root-tree [a,s] by MSAFREE:def 15;
y in (FreeSort the Sorts of MSA) . s by A22;
then A25: y in FreeSort ( the Sorts of MSA,s) by MSAFREE:def 11;
hence ( (IT29 . s) . y = x implies y = root-tree [x,s] ) by A20, A23, A24; :: thesis: ( S₁[s,x,y] implies (IT29 . s) . y = x )
assume y = root-tree [x,s] ; :: thesis: (IT29 . s) . y = x
then [x,s] = [a,s] by A24, TREES_4:4;
then x = a by ZFMISC_1:27;
hence (IT29 . s) . y = x by A20, A25, A23, A24; :: thesis: verum

end;

IT19 = IT29 from MSAFREE1:sch 3(A12, A14, A19, A21);
hence IT1 = IT2 ; :: thesis: verum