reconsider A = FreeGen the Sorts of MSA as free GeneratorSet of FreeEnv MSA by MSAFREE:16;

defpred S_{1}[ object , object ] means ex s being SortSymbol of S ex f being Function of (A . s),( the Sorts of MSA . s) st

( f = $2 & s = $1 & ( for x, y being set st y in A . s & y = root-tree [x,s] & x in the Sorts of MSA . s holds

f . y = x ) );

A1: for i being object st i in the carrier of S holds

ex j being object st S_{1}[i,j]

A7: for i being object st i in the carrier of S holds

S_{1}[i,f . i]
from PBOOLE:sch 3(A1);

consider IT being ManySortedFunction of (FreeEnv MSA),MSA such that

A8: IT is_homomorphism FreeEnv MSA,MSA and

A9: IT || A = f by MSAFREE:def 5;

take IT ; :: thesis: ( IT 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

(IT . s) . y = x ) )

thus IT is_homomorphism FreeEnv MSA,MSA by A8; :: thesis: 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

(IT . s) . y = x

let s be SortSymbol of S; :: thesis: 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

(IT . s) . y = x

let x, y be set ; :: thesis: ( y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s implies (IT . s) . y = x )

A10: ex t being SortSymbol of S ex g being Function of (A . t),( the Sorts of MSA . t) st

( g = f . s & t = s & ( for x, y being set st y in A . t & y = root-tree [x,t] & x in the Sorts of MSA . t holds

g . y = x ) ) by A7;

assume that

y in FreeSort ( the Sorts of MSA,s) and

A11: ( y = root-tree [x,s] & x in the Sorts of MSA . s ) ; :: thesis: (IT . s) . y = x

y in FreeGen (s, the Sorts of MSA) by A11, MSAFREE:def 15;

then A12: y in A . s by MSAFREE:def 16;

hence (IT . s) . y = ((IT . s) | (A . s)) . y by FUNCT_1:49

.= (f . s) . y by A9, MSAFREE:def 1

.= x by A11, A12, A10 ;

:: thesis: verum

defpred S

( f = $2 & s = $1 & ( for x, y being set st y in A . s & y = root-tree [x,s] & x in the Sorts of MSA . s holds

f . y = x ) );

A1: for i being object st i in the carrier of S holds

ex j being object st S

proof

consider f being ManySortedSet of the carrier of S such that
let i be object ; :: thesis: ( i in the carrier of S implies ex j being object st S_{1}[i,j] )

assume i in the carrier of S ; :: thesis: ex j being object st S_{1}[i,j]

then reconsider s = i as SortSymbol of S ;

defpred S_{2}[ object , object ] means $1 = root-tree [$2,s];

A2: for e being object st e in A . s holds

ex u being object st

( u in the Sorts of MSA . s & S_{2}[e,u] )

A4: ( dom j = A . s & rng j c= the Sorts of MSA . s & ( for e being object st e in A . s holds

S_{2}[e,j . e] ) )
from FUNCT_1:sch 6(A2);

reconsider f = j as Function of (A . s),( the Sorts of MSA . s) by A4, FUNCT_2:def 1, RELSET_1:4;

take j ; :: thesis: S_{1}[i,j]

take s ; :: thesis: ex f being Function of (A . s),( the Sorts of MSA . s) st

( f = j & s = i & ( for x, y being set st y in A . s & y = root-tree [x,s] & x in the Sorts of MSA . s holds

f . y = x ) )

take f ; :: thesis: ( f = j & s = i & ( for x, y being set st y in A . s & y = root-tree [x,s] & x in the Sorts of MSA . s holds

f . y = x ) )

thus ( f = j & s = i ) ; :: thesis: for x, y being set st y in A . s & y = root-tree [x,s] & x in the Sorts of MSA . s holds

f . y = x

let x, y be set ; :: thesis: ( y in A . s & y = root-tree [x,s] & x in the Sorts of MSA . s implies f . y = x )

assume that

A5: y in A . s and

A6: y = root-tree [x,s] and

x in the Sorts of MSA . s ; :: thesis: f . y = x

y = root-tree [(j . y),s] by A4, A5;

then [x,s] = [(j . y),s] by A6, TREES_4:4;

hence f . y = x by XTUPLE_0:1; :: thesis: verum

end;assume i in the carrier of S ; :: thesis: ex j being object st S

then reconsider s = i as SortSymbol of S ;

defpred S

A2: for e being object st e in A . s holds

ex u being object st

( u in the Sorts of MSA . s & S

proof

consider j being Function such that
let e be object ; :: thesis: ( e in A . s implies ex u being object st

( u in the Sorts of MSA . s & S_{2}[e,u] ) )

assume e in A . s ; :: thesis: ex u being object st

( u in the Sorts of MSA . s & S_{2}[e,u] )

then e in FreeGen (s, the Sorts of MSA) by MSAFREE:def 16;

then consider a being set such that

A3: ( a in the Sorts of MSA . s & e = root-tree [a,s] ) by MSAFREE:def 15;

thus ex u being object st

( u in the Sorts of MSA . s & S_{2}[e,u] )
by A3; :: thesis: verum

end;( u in the Sorts of MSA . s & S

assume e in A . s ; :: thesis: ex u being object st

( u in the Sorts of MSA . s & S

then e in FreeGen (s, the Sorts of MSA) by MSAFREE:def 16;

then consider a being set such that

A3: ( a in the Sorts of MSA . s & e = root-tree [a,s] ) by MSAFREE:def 15;

thus ex u being object st

( u in the Sorts of MSA . s & S

A4: ( dom j = A . s & rng j c= the Sorts of MSA . s & ( for e being object st e in A . s holds

S

reconsider f = j as Function of (A . s),( the Sorts of MSA . s) by A4, FUNCT_2:def 1, RELSET_1:4;

take j ; :: thesis: S

take s ; :: thesis: ex f being Function of (A . s),( the Sorts of MSA . s) st

( f = j & s = i & ( for x, y being set st y in A . s & y = root-tree [x,s] & x in the Sorts of MSA . s holds

f . y = x ) )

take f ; :: thesis: ( f = j & s = i & ( for x, y being set st y in A . s & y = root-tree [x,s] & x in the Sorts of MSA . s holds

f . y = x ) )

thus ( f = j & s = i ) ; :: thesis: for x, y being set st y in A . s & y = root-tree [x,s] & x in the Sorts of MSA . s holds

f . y = x

let x, y be set ; :: thesis: ( y in A . s & y = root-tree [x,s] & x in the Sorts of MSA . s implies f . y = x )

assume that

A5: y in A . s and

A6: y = root-tree [x,s] and

x in the Sorts of MSA . s ; :: thesis: f . y = x

y = root-tree [(j . y),s] by A4, A5;

then [x,s] = [(j . y),s] by A6, TREES_4:4;

hence f . y = x by XTUPLE_0:1; :: thesis: verum

A7: for i being object st i in the carrier of S holds

S

now :: thesis: for x being object st x in dom f holds

f . x is Function

then reconsider f = f as ManySortedFunction of the carrier of S by FUNCOP_1:def 6;f . x is Function

let x be object ; :: thesis: ( x in dom f implies f . x is Function )

assume x in dom f ; :: thesis: f . x is Function

then x in the carrier of S ;

then S_{1}[x,f . x]
by A7;

hence f . x is Function ; :: thesis: verum

end;assume x in dom f ; :: thesis: f . x is Function

then x in the carrier of S ;

then S

hence f . x is Function ; :: thesis: verum

now :: thesis: for i being object st i in the carrier of S holds

f . i is Function of (A . i),( the Sorts of MSA . i)

then reconsider f = f as ManySortedFunction of A, the Sorts of MSA by PBOOLE:def 15;f . i is Function of (A . i),( the Sorts of MSA . i)

let i be object ; :: thesis: ( i in the carrier of S implies f . i is Function of (A . i),( the Sorts of MSA . i) )

assume i in the carrier of S ; :: thesis: f . i is Function of (A . i),( the Sorts of MSA . i)

then S_{1}[i,f . i]
by A7;

hence f . i is Function of (A . i),( the Sorts of MSA . i) ; :: thesis: verum

end;assume i in the carrier of S ; :: thesis: f . i is Function of (A . i),( the Sorts of MSA . i)

then S

hence f . i is Function of (A . i),( the Sorts of MSA . i) ; :: thesis: verum

consider IT being ManySortedFunction of (FreeEnv MSA),MSA such that

A8: IT is_homomorphism FreeEnv MSA,MSA and

A9: IT || A = f by MSAFREE:def 5;

take IT ; :: thesis: ( IT 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

(IT . s) . y = x ) )

thus IT is_homomorphism FreeEnv MSA,MSA by A8; :: thesis: 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

(IT . s) . y = x

let s be SortSymbol of S; :: thesis: 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

(IT . s) . y = x

let x, y be set ; :: thesis: ( y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s implies (IT . s) . y = x )

A10: ex t being SortSymbol of S ex g being Function of (A . t),( the Sorts of MSA . t) st

( g = f . s & t = s & ( for x, y being set st y in A . t & y = root-tree [x,t] & x in the Sorts of MSA . t holds

g . y = x ) ) by A7;

assume that

y in FreeSort ( the Sorts of MSA,s) and

A11: ( y = root-tree [x,s] & x in the Sorts of MSA . s ) ; :: thesis: (IT . s) . y = x

y in FreeGen (s, the Sorts of MSA) by A11, MSAFREE:def 15;

then A12: y in A . s by MSAFREE:def 16;

hence (IT . s) . y = ((IT . s) | (A . s)) . y by FUNCT_1:49

.= (f . s) . y by A9, MSAFREE:def 1

.= x by A11, A12, A10 ;

:: thesis: verum