defpred S₁[ set , set ] means ex f being Function of ((FreeGen F₃()) . $1),(the Sorts of F₂() . $1) st
( $2 = f & ( for x being Element of F₃() . $1 holds f . (root-tree [x,$1]) = F₄(x,$1) ) );
A2: for a being set st a in the carrier of F₁() holds
ex y being set st S₁[a,y]

proof

let a be set ; :: thesis: ( a in the carrier of F₁() implies ex y being set st S₁[a,y] )
assume a in the carrier of F₁() ; :: thesis: ex y being set st S₁[a,y]
then reconsider s = a as SortSymbol of F₁() ;
defpred S₂[ set , set ] means ex x being Element of F₃() . s st
( $1 = root-tree [x,s] & $2 = F₄(x,s) );
A3: (FreeGen F₃()) . s = FreeGen s,F₃() by MSAFREE:def 18;
A4: for y being set st y in (FreeGen F₃()) . s holds
ex z being set st
( z in the Sorts of F₂() . s & S₂[y,z] )

proof

let y be set ; :: thesis: ( y in (FreeGen F₃()) . s implies ex z being set st
( z in the Sorts of F₂() . s & S₂[y,z] ) )
assume y in (FreeGen F₃()) . s ; :: thesis: ex z being set st
( z in the Sorts of F₂() . s & S₂[y,z] )
then consider a being set such that
A5: a in F₃() . s and
A6: y = root-tree [a,s] by A3, MSAFREE:def 17;
reconsider a = a as Element of F₃() . s by A5;
take z = F₄(a,s); :: thesis: ( z in the Sorts of F₂() . s & S₂[y,z] )
thus z in the Sorts of F₂() . s by A1; :: thesis: S₂[y,z]
take a ; :: thesis: ( y = root-tree [a,s] & z = F₄(a,s) )
thus ( y = root-tree [a,s] & z = F₄(a,s) ) by A6; :: thesis: verum

end;

consider f being Function such that
A7: ( dom f = (FreeGen F₃()) . s & rng f c= the Sorts of F₂() . s ) and
A8: for y being set st y in (FreeGen F₃()) . s holds
S₂[y,f . y] from WELLORD2:sch 1(A4);
reconsider f = f as Function of ((FreeGen F₃()) . a),(the Sorts of F₂() . a) by A7, FUNCT_2:4;
take y = f; :: thesis: S₁[a,y]
take f ; :: thesis: ( y = f & ( for x being Element of F₃() . a holds f . (root-tree [x,a]) = F₄(x,a) ) )
thus y = f ; :: thesis: for x being Element of F₃() . a holds f . (root-tree [x,a]) = F₄(x,a)
let x be Element of F₃() . a; :: thesis: f . (root-tree [x,a]) = F₄(x,a)
root-tree [x,s] in (FreeGen F₃()) . s by A3, MSAFREE:def 17;
then consider z being Element of F₃() . s such that
A9: root-tree [x,s] = root-tree [z,s] and
A10: f . (root-tree [x,s]) = F₄(z,s) by A8;
[x,s] = [z,s] by A9, TREES_4:4;
hence f . (root-tree [x,a]) = F₄(x,a) by A10, ZFMISC_1:33; :: thesis: verum

end;

consider h being Function such that
A11: dom h = the carrier of F₁() and
A12: for a being set st a in the carrier of F₁() holds
S₁[a,h . a] from CLASSES1:sch 1(A2);
reconsider h = h as ManySortedSet of the carrier of F₁() by A11, PARTFUN1:def 4, RELAT_1:def 18;
h is ManySortedFunction of FreeGen F₃(),the Sorts of F₂()

proof

let a be set ; :: according to PBOOLE:def 18 :: thesis: ( not a in the carrier of F₁() or h . a is Element of bool [:((FreeGen F₃()) . a),(the Sorts of F₂() . a):] )
assume a in the carrier of F₁() ; :: thesis: h . a is Element of bool [:((FreeGen F₃()) . a),(the Sorts of F₂() . a):]
then ex f being Function of ((FreeGen F₃()) . a),(the Sorts of F₂() . a) st
( h . a = f & ( for x being Element of F₃() . a holds f . (root-tree [x,a]) = F₄(x,a) ) ) by A12;
hence h . a is Element of bool [:((FreeGen F₃()) . a),(the Sorts of F₂() . a):] ; :: thesis: verum

end;

then reconsider h = h as ManySortedFunction of FreeGen F₃(),the Sorts of F₂() ;
consider H being ManySortedFunction of (FreeMSA F₃()),F₂() such that
A13: H is_homomorphism FreeMSA F₃(),F₂() and
A14: H || (FreeGen F₃()) = h by MSAFREE:def 5;
take H ; :: thesis: ( H is_homomorphism FreeMSA F₃(),F₂() & ( for s being SortSymbol of F₁()
for x being Element of F₃() . s holds (H . s) . (root-tree [x,s]) = F₄(x,s) ) )
thus H is_homomorphism FreeMSA F₃(),F₂() by A13; :: thesis: for s being SortSymbol of F₁()
for x being Element of F₃() . s holds (H . s) . (root-tree [x,s]) = F₄(x,s)
let s be SortSymbol of F₁(); :: thesis: for x being Element of F₃() . s holds (H . s) . (root-tree [x,s]) = F₄(x,s)
let x be Element of F₃() . s; :: thesis: (H . s) . (root-tree [x,s]) = F₄(x,s)
A15: ex f being Function of ((FreeGen F₃()) . s),(the Sorts of F₂() . s) st
( h . s = f & ( for x being Element of F₃() . s holds f . (root-tree [x,s]) = F₄(x,s) ) ) by A12;
reconsider t = root-tree [x,s] as Term of F₁(),F₃() by MSATERM:4;
(FreeGen F₃()) . s = FreeGen s,F₃() by MSAFREE:def 18;
then A16: t in (FreeGen F₃()) . s by MSAFREE:def 17;
h . s = (H . s) | ((FreeGen F₃()) . s) by A14, MSAFREE:def 1;
then (H . s) . (root-tree [x,s]) = (h . s) . (root-tree [x,s]) by A16, FUNCT_1:72;
hence (H . s) . (root-tree [x,s]) = F₄(x,s) by A15; :: thesis: verum