defpred S_{1}[ object , object ] means ex f being Function of ((FreeGen F_{3}()) . $1),( the Sorts of F_{2}() . $1) st

( $2 = f & ( for x being Element of F_{3}() . $1 holds f . (root-tree [x,$1]) = F_{4}(x,$1) ) );

A2: for a being object st a in the carrier of F_{1}() holds

ex y being object st S_{1}[a,y]

A11: dom h = the carrier of F_{1}()
and

A12: for a being object st a in the carrier of F_{1}() holds

S_{1}[a,h . a]
from CLASSES1:sch 1(A2);

reconsider h = h as ManySortedSet of the carrier of F_{1}() by A11, PARTFUN1:def 2, RELAT_1:def 18;

h is ManySortedFunction of FreeGen F_{3}(), the Sorts of F_{2}()
_{3}(), the Sorts of F_{2}() ;

consider H being ManySortedFunction of (FreeMSA F_{3}()),F_{2}() such that

A13: H is_homomorphism FreeMSA F_{3}(),F_{2}()
and

A14: H || (FreeGen F_{3}()) = h
by MSAFREE:def 5;

take H ; :: thesis: ( H is_homomorphism FreeMSA F_{3}(),F_{2}() & ( for s being SortSymbol of F_{1}()

for x being Element of F_{3}() . s holds (H . s) . (root-tree [x,s]) = F_{4}(x,s) ) )

thus H is_homomorphism FreeMSA F_{3}(),F_{2}()
by A13; :: thesis: for s being SortSymbol of F_{1}()

for x being Element of F_{3}() . s holds (H . s) . (root-tree [x,s]) = F_{4}(x,s)

let s be SortSymbol of F_{1}(); :: thesis: for x being Element of F_{3}() . s holds (H . s) . (root-tree [x,s]) = F_{4}(x,s)

let x be Element of F_{3}() . s; :: thesis: (H . s) . (root-tree [x,s]) = F_{4}(x,s)

A15: ex f being Function of ((FreeGen F_{3}()) . s),( the Sorts of F_{2}() . s) st

( h . s = f & ( for x being Element of F_{3}() . s holds f . (root-tree [x,s]) = F_{4}(x,s) ) )
by A12;

reconsider t = root-tree [x,s] as Term of F_{1}(),F_{3}() by MSATERM:4;

(FreeGen F_{3}()) . s = FreeGen (s,F_{3}())
by MSAFREE:def 16;

then A16: t in (FreeGen F_{3}()) . s
by MSAFREE:def 15;

h . s = (H . s) | ((FreeGen F_{3}()) . s)
by A14, MSAFREE:def 1;

then (H . s) . (root-tree [x,s]) = (h . s) . (root-tree [x,s]) by A16, FUNCT_1:49;

hence (H . s) . (root-tree [x,s]) = F_{4}(x,s)
by A15; :: thesis: verum

( $2 = f & ( for x being Element of F

A2: for a being object st a in the carrier of F

ex y being object st S

proof

consider h being Function such that
let a be object ; :: thesis: ( a in the carrier of F_{1}() implies ex y being object st S_{1}[a,y] )

assume a in the carrier of F_{1}()
; :: thesis: ex y being object st S_{1}[a,y]

then reconsider s = a as SortSymbol of F_{1}() ;

defpred S_{2}[ object , object ] means ex x being Element of F_{3}() . s st

( $1 = root-tree [x,s] & $2 = F_{4}(x,s) );

A3: (FreeGen F_{3}()) . s = FreeGen (s,F_{3}())
by MSAFREE:def 16;

A4: for y being object st y in (FreeGen F_{3}()) . s holds

ex z being object st

( z in the Sorts of F_{2}() . s & S_{2}[y,z] )

A7: ( dom f = (FreeGen F_{3}()) . s & rng f c= the Sorts of F_{2}() . s )
and

A8: for y being object st y in (FreeGen F_{3}()) . s holds

S_{2}[y,f . y]
from FUNCT_1:sch 6(A4);

reconsider f = f as Function of ((FreeGen F_{3}()) . a),( the Sorts of F_{2}() . a) by A7, FUNCT_2:2;

take y = f; :: thesis: S_{1}[a,y]

take f ; :: thesis: ( y = f & ( for x being Element of F_{3}() . a holds f . (root-tree [x,a]) = F_{4}(x,a) ) )

thus y = f ; :: thesis: for x being Element of F_{3}() . a holds f . (root-tree [x,a]) = F_{4}(x,a)

let x be Element of F_{3}() . a; :: thesis: f . (root-tree [x,a]) = F_{4}(x,a)

root-tree [x,s] in (FreeGen F_{3}()) . s
by A3, MSAFREE:def 15;

then consider z being Element of F_{3}() . s such that

A9: root-tree [x,s] = root-tree [z,s] and

A10: f . (root-tree [x,s]) = F_{4}(z,s)
by A8;

[x,s] = [z,s] by A9, TREES_4:4;

hence f . (root-tree [x,a]) = F_{4}(x,a)
by A10, XTUPLE_0:1; :: thesis: verum

end;assume a in the carrier of F

then reconsider s = a as SortSymbol of F

defpred S

( $1 = root-tree [x,s] & $2 = F

A3: (FreeGen F

A4: for y being object st y in (FreeGen F

ex z being object st

( z in the Sorts of F

proof

consider f being Function such that
let y be object ; :: thesis: ( y in (FreeGen F_{3}()) . s implies ex z being object st

( z in the Sorts of F_{2}() . s & S_{2}[y,z] ) )

assume y in (FreeGen F_{3}()) . s
; :: thesis: ex z being object st

( z in the Sorts of F_{2}() . s & S_{2}[y,z] )

then consider a being set such that

A5: a in F_{3}() . s
and

A6: y = root-tree [a,s] by A3, MSAFREE:def 15;

reconsider a = a as Element of F_{3}() . s by A5;

take z = F_{4}(a,s); :: thesis: ( z in the Sorts of F_{2}() . s & S_{2}[y,z] )

thus z in the Sorts of F_{2}() . s
by A1; :: thesis: S_{2}[y,z]

take a ; :: thesis: ( y = root-tree [a,s] & z = F_{4}(a,s) )

thus ( y = root-tree [a,s] & z = F_{4}(a,s) )
by A6; :: thesis: verum

end;( z in the Sorts of F

assume y in (FreeGen F

( z in the Sorts of F

then consider a being set such that

A5: a in F

A6: y = root-tree [a,s] by A3, MSAFREE:def 15;

reconsider a = a as Element of F

take z = F

thus z in the Sorts of F

take a ; :: thesis: ( y = root-tree [a,s] & z = F

thus ( y = root-tree [a,s] & z = F

A7: ( dom f = (FreeGen F

A8: for y being object st y in (FreeGen F

S

reconsider f = f as Function of ((FreeGen F

take y = f; :: thesis: S

take f ; :: thesis: ( y = f & ( for x being Element of F

thus y = f ; :: thesis: for x being Element of F

let x be Element of F

root-tree [x,s] in (FreeGen F

then consider z being Element of F

A9: root-tree [x,s] = root-tree [z,s] and

A10: f . (root-tree [x,s]) = F

[x,s] = [z,s] by A9, TREES_4:4;

hence f . (root-tree [x,a]) = F

A11: dom h = the carrier of F

A12: for a being object st a in the carrier of F

S

reconsider h = h as ManySortedSet of the carrier of F

h is ManySortedFunction of FreeGen F

proof

then reconsider h = h as ManySortedFunction of FreeGen F
let a be object ; :: according to PBOOLE:def 15 :: thesis: ( not a in the carrier of F_{1}() or h . a is Element of bool [:((FreeGen F_{3}()) . a),( the Sorts of F_{2}() . a):] )

assume a in the carrier of F_{1}()
; :: thesis: h . a is Element of bool [:((FreeGen F_{3}()) . a),( the Sorts of F_{2}() . a):]

then ex f being Function of ((FreeGen F_{3}()) . a),( the Sorts of F_{2}() . a) st

( h . a = f & ( for x being Element of F_{3}() . a holds f . (root-tree [x,a]) = F_{4}(x,a) ) )
by A12;

hence h . a is Element of bool [:((FreeGen F_{3}()) . a),( the Sorts of F_{2}() . a):]
; :: thesis: verum

end;assume a in the carrier of F

then ex f being Function of ((FreeGen F

( h . a = f & ( for x being Element of F

hence h . a is Element of bool [:((FreeGen F

consider H being ManySortedFunction of (FreeMSA F

A13: H is_homomorphism FreeMSA F

A14: H || (FreeGen F

take H ; :: thesis: ( H is_homomorphism FreeMSA F

for x being Element of F

thus H is_homomorphism FreeMSA F

for x being Element of F

let s be SortSymbol of F

let x be Element of F

A15: ex f being Function of ((FreeGen F

( h . s = f & ( for x being Element of F

reconsider t = root-tree [x,s] as Term of F

(FreeGen F

then A16: t in (FreeGen F

h . s = (H . s) | ((FreeGen F

then (H . s) . (root-tree [x,s]) = (h . s) . (root-tree [x,s]) by A16, FUNCT_1:49;

hence (H . s) . (root-tree [x,s]) = F