let S be non empty non void ManySortedSign ; :: thesis:
let X0 be non-empty countable ManySortedSet of S; :: thesis:
let A0 be X0,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis:
set A = A0;
let h be ManySortedFunction of (TermAlg S),A0; :: thesis:
assume A1: h is_homomorphism TermAlg S,A0 ; :: thesis:
let v be ManySortedFunction of X0, the carrier of S --> NAT; :: thesis:
assume A2: v is "1-1" ; :: thesis:
set Z = the carrier of S --> NAT;
deffunc H₂( object ) -> set = (NAT --> the Element of X0 . $1) +* ((v . $1) ");
consider w being ManySortedSet of S such that
A3: for s being SortSymbol of S holds w . s = H₂(s) from PBOOLE:sch 5();
w is Function-yielding

proof

let x be object ; :: according to FUNCOP_1:def 6 :: thesis:
assume x in dom w ; :: thesis:
then w . x = H₂(x) by A3;
hence w . x is set ; :: thesis:

end;

then reconsider w = w as ManySortedFunction of the carrier of S ;
w is ManySortedFunction of the carrier of S --> NAT,X0

proof

let x be object ; :: according to PBOOLE:def 15 :: thesis:
assume x in the carrier of S ; :: thesis:
then reconsider s = x as SortSymbol of S ;
dom v = the carrier of S by PARTFUN1:def 2;
then A4: ( w . x = H₂(s) & v . s is one-to-one & ( the carrier of S --> NAT) . s = NAT & rng (v . s) c= ( the carrier of S --> NAT) . s ) by A2, A3;
then A5: dom (w . s) = (dom (NAT --> the Element of X0 . s)) \/ (dom ((v . s) ")) by FUNCT_4:def 1
.= NAT \/ (dom ((v . s) "))
.= NAT \/ (rng (v . s)) by A4, FUNCT_1:33
.= NAT by XBOOLE_1:12 ;
rng (w . s) c= X0 . s

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng (w . s) ; :: thesis:
then consider y being object such that
A7: ( y in dom (w . s) & x = (w . s) . y ) by FUNCT_1:def 3;
( y in dom ((v . s) ") or y nin dom ((v . s) ") ) ;
then ( ( x = ((v . s) ") . y & y in dom ((v . s) ") & dom v = the carrier of S ) or x = (NAT --> the Element of X0 . s) . y ) by A4, A7, FUNCT_4:11, FUNCT_4:13, PARTFUN1:def 2;
then ( ( x = ((v . s) ") . y & y in dom ((v . s) ") & v . s is one-to-one ) or x = the Element of X0 . s ) by A2, A5, A7, FUNCOP_1:7;
then ( ( x in rng ((v . s) ") & rng ((v . s) ") = dom (v . s) & dom (v . s) c= X0 . s ) or x in X0 . s ) by FUNCT_1:33, FUNCT_1:def 3;
hence x in X0 . s ; :: thesis:

end;

hence w . x is Element of bool [:(( the carrier of S --> NAT) . x),(X0 . x):] by A5, FUNCT_2:2; :: thesis:

end;

then reconsider w = w as ManySortedFunction of the carrier of S --> NAT,X0 ;
consider ww being ManySortedFunction of (TermAlg S),A0 such that
A8: ( ww is_homomorphism TermAlg S,A0 & ( for s being SortSymbol of S
for i being Nat holds (ww . s) . (root-tree [i,s]) = root-tree [((w . s) . i),s] ) ) by Th62;
A9: dom v = the carrier of S by PARTFUN1:def 2;
rngs v c= the carrier of S --> NAT

proof

let s be object ; :: according to PBOOLE:def 2 :: thesis:
assume s in the carrier of S ; :: thesis:
then (rngs v) . s = rng (v . s) by A9, FUNCT_6:22;
hence (rngs v) . s c= ( the carrier of S --> NAT) . s ; :: thesis:

end;

then reconsider Y = rngs v as non-empty ManySortedSubset of the carrier of S --> NAT by PBOOLE:def 18;
take Y ; :: thesis:
A10: Free (S,( the carrier of S --> NAT)) = TermAlg S by MSAFREE3:31;
A11: Free (S,Y) is MSSubAlgebra of Free (S,( the carrier of S --> NAT)) by Th59;
then reconsider B = the Sorts of (Free (S,Y)) as MSSubset of (TermAlg S) by A10, MSUALG_2:def 9;
take B ; :: thesis:
reconsider wB = ww || B as ManySortedFunction of (Free (S,Y)),A0 ;
take wB ; :: thesis:
reconsider G = FreeGen X0 as GeneratorSet of A0 by Th45;
consider vv being ManySortedFunction of G, the Sorts of (TermAlg S) such that
A12: for s being SortSymbol of S
for i being Element of X0 . s holds (vv . s) . (root-tree [i,s]) = root-tree [((v . s) . i),s] by Th63;
consider g being ManySortedFunction of A0,A0 such that
A13: ( g is_homomorphism A0,A0 & g || G = h ** vv ) by Def9;
take g ; :: thesis:
thus ( Y = rngs v & B = the Sorts of (Free (S,Y)) ) ; :: thesis:
Free (S,Y) = FreeMSA (rngs v) by MSAFREE3:31;
hence FreeGen (rngs v) c= B by PBOOLE:def 18; :: thesis:
thus ( wB is_homomorphism Free (S,Y),A0 & g is_homomorphism A0,A0 ) by A13, A8, A10, A11, EQUATION:22; :: thesis:
then A14: g ** wB is_homomorphism Free (S,Y),A0 by MSUALG_3:10;
reconsider H = FreeGen Y as GeneratorSet of Free (S,Y) by MSAFREE3:31;
reconsider hB = h || B as ManySortedFunction of (Free (S,Y)),A0 ;

A15: now :: thesis:

let x be object ; :: thesis:
assume x in the carrier of S ; :: thesis:
then reconsider s = x as SortSymbol of S ;
A16: ( dom ((hB || H) . s) = H . s & dom (((g ** wB) || H) . s) = H . s ) by FUNCT_2:def 1;

now :: thesis:

let y be object ; :: thesis:
assume A17: y in H . s ; :: thesis:
then y in FreeGen (s,Y) by MSAFREE:def 16;
then consider z being set such that
A18: ( z in Y . s & y = root-tree [z,s] ) by MSAFREE:def 15;
A19: ( H . s c= B . s & Y . s c= ( the carrier of S --> NAT) . s ) by PBOOLE:def 2, PBOOLE:def 18;
then A20: (w . s) . z in X0 . s by A18, FUNCT_2:5;
( wB . s = (ww . s) | (B . s) & z in ( the carrier of S --> NAT) . s ) by A18, A19, MSAFREE:def 1;
then A21: ( (wB . s) . y = (ww . s) . y & z in NAT ) by A17, A19, FUNCT_1:49;
then (wB . s) . y = root-tree [((w . s) . z),s] by A8, A18;
then (wB . s) . y in FreeGen (s,X0) by A20, MSAFREE:def 15;
then A22: (wB . s) . y in G . s by MSAFREE:def 16;
z in ( the carrier of S --> NAT) . s by A18, A19;
then z in NAT ;
then A23: (vv . s) . ((ww . s) . y) = (vv . s) . (root-tree [((w . s) . z),s]) by A8, A18
.= root-tree [((v . s) . ((w . s) . z)),s] by A12, A20
.= root-tree [((v . s) . (((NAT --> the Element of X0 . s) +* ((v . s) ")) . z)),s] by A3 ;
dom v = the carrier of S by PARTFUN1:def 2;
then A24: ( v . s is one-to-one & rng (v . s) = Y . s ) by A2, FUNCT_6:22;
A25: z in dom ((v . s) ") by A18, A24, FUNCT_1:33;
A26: (vv . s) . ((ww . s) . y) = root-tree [((v . s) . (((v . s) ") . z)),s] by A23, A25, FUNCT_4:13
.= y by A18, A24, FUNCT_1:35 ;
A27: rngs vv c= B

proof

let x be object ; :: according to PBOOLE:def 2 :: thesis:
assume x in the carrier of S ; :: thesis:
then reconsider s = x as SortSymbol of S ;
let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A28: y in (rngs vv) . x ; :: thesis:
dom vv = the carrier of S by PARTFUN1:def 2;
then y in rng (vv . s) by A28, FUNCT_6:22;
then consider z being object such that
A29: ( z in dom (vv . s) & y = (vv . s) . z ) by FUNCT_1:def 3;
dom (vv . s) = G . s by FUNCT_2:def 1
.= FreeGen (s,X0) by MSAFREE:def 16 ;
then consider a being set such that
A30: ( a in X0 . s & z = root-tree [a,s] ) by A29, MSAFREE:def 15;
( (v . s) . a in rng (v . s) & dom v = the carrier of S ) by A30, FUNCT_2:4, PARTFUN1:def 2;
then ( (v . s) . a in Y . s & y = root-tree [((v . s) . a),s] ) by A29, A30, A12, FUNCT_6:22;
then y in FreeGen (s,Y) by MSAFREE:def 15;
then ( y in H . s & H . s c= B . s ) by MSAFREE:def 16, PBOOLE:def 2, PBOOLE:def 18;
hence y in B . x ; :: thesis:

end;

A31: dom (hB ** vv) = the carrier of S /\ the carrier of S by PARTFUN1:def 2;
A32: dom (g ** wB) = the carrier of S /\ the carrier of S by PARTFUN1:def 2;
thus ((hB || H) . x) . y = ((hB . s) | (H . s)) . y by MSAFREE:def 1
.= (hB . s) . y by A17, FUNCT_1:49
.= ((hB . s) * (vv . s)) . ((wB . s) . y) by A26, A21, A22, FUNCT_2:15
.= ((hB ** vv) . s) . ((wB . s) . y) by A31, PBOOLE:def 19
.= ((g || G) . s) . ((wB . s) . y) by A13, A27, EXTENS_1:11
.= ((g . s) | (G . s)) . ((wB . s) . y) by MSAFREE:def 1
.= (g . s) . ((wB . s) . y) by A22, FUNCT_1:49
.= ((g . s) * (wB . s)) . y by A19, A17, FUNCT_2:15
.= ((g ** wB) . s) . y by A32, PBOOLE:def 19
.= (((g ** wB) . s) | (H . s)) . y by A17, FUNCT_1:49
.= (((g ** wB) || H) . x) . y by MSAFREE:def 1 ; :: thesis:

end;

hence (hB || H) . x = ((g ** wB) || H) . x by A16; :: thesis:

end;

hB is_homomorphism Free (S,Y),A0 by A1, A11, A10, EQUATION:22;
hence h || B = g ** wB by A15, A14, EXTENS_1:19, PBOOLE:3; :: thesis:
let s be SortSymbol of S; :: thesis:
let i be Nat; :: thesis:
assume A33: i in Y . s ; :: thesis:
A34: dom v = the carrier of S by PARTFUN1:def 2;
then A35: v . s is one-to-one by A2;
then A36: ( rng ((v . s) ") = dom (v . s) & dom (v . s) = X0 . s & rng (v . s) = Y . s & dom ((v . s) ") = rng (v . s) ) by A34, FUNCT_1:33, FUNCT_2:def 1, FUNCT_6:22;
then reconsider x = ((v . s) ") . i as Element of X0 . s by A33, FUNCT_1:def 3;
take x ; :: thesis:
thus (v . s) . x = i by A33, A35, A36, FUNCT_1:35; :: thesis:
( root-tree [i,s] in FreeGen (s,Y) & H c= B ) by A33, PBOOLE:def 18, MSAFREE:def 15;
then A37: ( root-tree [i,s] in H . s & H . s c= B . s ) by MSAFREE:def 16;
w . s = H₂(s) by A3;
then x = (w . s) . i by A33, A36, FUNCT_4:13;
then root-tree [x,s] = (ww . s) . (root-tree [i,s]) by A8
.= ((ww . s) | (B . s)) . (root-tree [i,s]) by A37, FUNCT_1:49 ;
hence (wB . s) . (root-tree [i,s]) = root-tree [x,s] by MSAFREE:def 1; :: thesis: