defpred S_{1}[ 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_{1}[s,x,y] )

( 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_{1}[s,x,y] )

hence IT1 = IT2 ; :: thesis: verum

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

proof

assume
IT2 is_homomorphism FreeEnv MSA,MSA
; :: thesis: ( ex s being SortSymbol of S ex x, y being set st
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_{1}[s,x,y] )

let x, y be set ; :: thesis: ( y in FreeGen (s, the Sorts of MSA) implies ( (IT19 . s) . y = x iff S_{1}[s,x,y] ) )

assume A16: y in FreeGen (s, the Sorts of MSA) ; :: thesis: ( (IT19 . s) . y = x iff S_{1}[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_{1}[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;( (IT19 . s) . y = x iff S

let x, y be set ; :: thesis: ( y in FreeGen (s, the Sorts of MSA) implies ( (IT19 . s) . y = x iff S

assume A16: y in FreeGen (s, the Sorts of MSA) ; :: thesis: ( (IT19 . s) . y = x iff S

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

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

( 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

proof

IT19 = IT29
from MSAFREE1:sch 3(A13, A15, A20, A22);
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_{1}[s,x,y] )

let x, y be set ; :: thesis: ( y in FreeGen (s, the Sorts of MSA) implies ( (IT29 . s) . y = x iff S_{1}[s,x,y] ) )

assume A23: y in FreeGen (s, the Sorts of MSA) ; :: thesis: ( (IT29 . s) . y = x iff S_{1}[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_{1}[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;( (IT29 . s) . y = x iff S

let x, y be set ; :: thesis: ( y in FreeGen (s, the Sorts of MSA) implies ( (IT29 . s) . y = x iff S

assume A23: y in FreeGen (s, the Sorts of MSA) ; :: thesis: ( (IT29 . s) . y = x iff S

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

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

hence IT1 = IT2 ; :: thesis: verum