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 A13: IT19 is_homomorphism FreeMSA the Sorts of MSA,MSA ;
assume A14: 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 )
A15: 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 A16: 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
A17: a in the Sorts of MSA . s and
A18: y = root-tree [a,s] by MSAFREE:def 15;
y in (FreeSort the Sorts of MSA) . s by A16;
then A19: y in FreeSort ( the Sorts of MSA,s) by MSAFREE:def 11;
hence ( (IT19 . s) . y = x implies y = root-tree [x,s] ) by A14, A17, A18; :: 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 A18, TREES_4:4;
then x = a by XTUPLE_0:1;
hence (IT19 . s) . y = x by A14, A19, A17, A18; :: 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 A20: IT29 is_homomorphism FreeMSA the Sorts of MSA,MSA ;
assume A21: 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
A22: 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 A23: 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
A24: a in the Sorts of MSA . s and
A25: y = root-tree [a,s] by MSAFREE:def 15;
y in (FreeSort the Sorts of MSA) . s by A23;
then A26: y in FreeSort ( the Sorts of MSA,s) by MSAFREE:def 11;
hence ( (IT29 . s) . y = x implies y = root-tree [x,s] ) by A21, A24, A25; :: 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 A25, TREES_4:4;
then x = a by XTUPLE_0:1;
hence (IT29 . s) . y = x by A21, A26, A24, A25; :: thesis: verum

end;

IT19 = IT29 from MSAFREE1:sch 3(A13, A15, A20, A22);
hence IT1 = IT2 ; :: thesis: verum