defpred S1[ object , object ] means ex f being Function of ((FreeGen F3()) . $1),( the Sorts of F2() . $1) st
( $2 = f & ( for x being Element of F3() . $1 holds f . (root-tree [x,$1]) = F4(x,$1) ) );
A2: for a being object st a in the carrier of F1() holds
ex y being object st S1[a,y]
proof
let a be object ; :: thesis: ( a in the carrier of F1() implies ex y being object st S1[a,y] )
assume a in the carrier of F1() ; :: thesis: ex y being object st S1[a,y]
then reconsider s = a as SortSymbol of F1() ;
defpred S2[ object , object ] means ex x being Element of F3() . s st
( $1 = root-tree [x,s] & $2 = F4(x,s) );
A3: (FreeGen F3()) . s = FreeGen (s,F3()) by MSAFREE:def 16;
A4: for y being object st y in (FreeGen F3()) . s holds
ex z being object st
( z in the Sorts of F2() . s & S2[y,z] )
proof
let y be object ; :: thesis: ( y in (FreeGen F3()) . s implies ex z being object st
( z in the Sorts of F2() . s & S2[y,z] ) )
assume y in (FreeGen F3()) . s ; :: thesis: ex z being object st
( z in the Sorts of F2() . s & S2[y,z] )
then consider a being set such that
A5: a in F3() . s and
A6: y = root-tree [a,s] by A3, MSAFREE:def 15;
reconsider a = a as Element of F3() . s by A5;
take z = F4(a,s); :: thesis: ( z in the Sorts of F2() . s & S2[y,z] )
thus z in the Sorts of F2() . s by A1; :: thesis: S2[y,z]
take a ; :: thesis: ( y = root-tree [a,s] & z = F4(a,s) )
thus ( y = root-tree [a,s] & z = F4(a,s) ) by A6; :: thesis: verum
end;
consider f being Function such that
A7: ( dom f = (FreeGen F3()) . s & rng f c= the Sorts of F2() . s ) and
A8: for y being object st y in (FreeGen F3()) . s holds
S2[y,f . y] from FUNCT_1:sch 6(A4);
 reconsider f = f as Function of ((FreeGen F3()) . a),( the Sorts of F2() . a) by A7, FUNCT_2:2;
take y = f; :: thesis: S1[a,y]
take f ; :: thesis: ( y = f & ( for x being Element of F3() . a holds f . (root-tree [x,a]) = F4(x,a) ) )
thus y = f ; :: thesis: for x being Element of F3() . a holds f . (root-tree [x,a]) = F4(x,a)
let x be Element of F3() . a; :: thesis: f . (root-tree [x,a]) = F4(x,a)
root-tree [x,s] in (FreeGen F3()) . s by A3, MSAFREE:def 15;
then consider z being Element of F3() . s such that
A9: root-tree [x,s] = root-tree [z,s] and
A10: f . (root-tree [x,s]) = F4(z,s) by A8;
[x,s] = [z,s] by A9, TREES_4:4;
hence f . (root-tree [x,a]) = F4(x,a) by A10, XTUPLE_0:1; :: thesis: verum
end;
consider h being Function such that
A11: dom h = the carrier of F1() and
A12: for a being object st a in the carrier of F1() holds
S1[a,h . a] from CLASSES1:sch 1(A2);
 reconsider h = h as ManySortedSet of the carrier of F1() by A11, PARTFUN1:def 2, RELAT_1:def 18;
h is ManySortedFunction of FreeGen F3(), the Sorts of F2()
proof
let a be object ; :: according to PBOOLE:def 15 :: thesis: ( not a in the carrier of F1() or h . a is Element of bool [:((FreeGen F3()) . a),( the Sorts of F2() . a):] )
assume a in the carrier of F1() ; :: thesis: h . a is Element of bool [:((FreeGen F3()) . a),( the Sorts of F2() . a):]
then ex f being Function of ((FreeGen F3()) . a),( the Sorts of F2() . a) st
( h . a = f & ( for x being Element of F3() . a holds f . (root-tree [x,a]) = F4(x,a) ) ) by A12;
hence h . a is Element of bool [:((FreeGen F3()) . a),( the Sorts of F2() . a):] ; :: thesis: verum
end;
then reconsider h = h as ManySortedFunction of FreeGen F3(), the Sorts of F2() ;
consider H being ManySortedFunction of (FreeMSA F3()),F2() such that
A13: H is_homomorphism FreeMSA F3(),F2() and
A14: H || (FreeGen F3()) = h by MSAFREE:def 5;
take H ; :: thesis: ( H is_homomorphism FreeMSA F3(),F2() & ( for s being SortSymbol of F1()
for x being Element of F3() . s holds (H . s) . (root-tree [x,s]) = F4(x,s) ) )
thus H is_homomorphism FreeMSA F3(),F2() by A13; :: thesis: for s being SortSymbol of F1()
for x being Element of F3() . s holds (H . s) . (root-tree [x,s]) = F4(x,s)
let s be SortSymbol of F1(); :: thesis: for x being Element of F3() . s holds (H . s) . (root-tree [x,s]) = F4(x,s)
let x be Element of F3() . s; :: thesis: (H . s) . (root-tree [x,s]) = F4(x,s)
A15: ex f being Function of ((FreeGen F3()) . s),( the Sorts of F2() . s) st
( h . s = f & ( for x being Element of F3() . s holds f . (root-tree [x,s]) = F4(x,s) ) ) by A12;
reconsider t = root-tree [x,s] as Term of F1(),F3() by MSATERM:4;
(FreeGen F3()) . s = FreeGen (s,F3()) by MSAFREE:def 16;
then A16: t in (FreeGen F3()) . s by MSAFREE:def 15;
h . s = (H . s) | ((FreeGen F3()) . 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]) = F4(x,s) by A15; :: thesis: verum