reconsider H = FreeGen X as ManySortedSubset of the generators of G by A1;
reconsider I = FreeGen X as GeneratorSet of A by MSAFREE4:45;
reconsider f1 = s as ManySortedFunction of the generators of G, the Sorts of C by Th43;
set g = f1 || H;
set r0 = r;
defpred S₁[ object , object ] means ex f being Function st
( f = $2 & dom f = H . $1 & ( $1 = r & t in H . r implies f . t = v ) & ( for r being SortSymbol of S st $1 = r holds
for x being Element of H . r st ( r = r implies x <> t ) holds
( ( x nin (vf t) . r implies f . x = ((f1 || H) . r) . x ) & ( x in (vf t) . r implies for q being Element of A,r st q = ((supp-term t) . r) . x holds
for u being ManySortedFunction of H, the Sorts of C st u = (f1 || H) +* (r,(supp-var t),v) holds
f . x = q value_at (C,u) ) ) ) );
A2: for x being object st x in the carrier of S holds
ex y being object st S₁[x,y]

let x be object ; :: thesis:
assume x in the carrier of S ; :: thesis:
then reconsider p = x as SortSymbol of S ;
defpred S₂[ object , object ] means ( ( p = r & $1 = t implies $2 = v ) & ( ( p = r implies $1 <> t ) implies ( ( $1 nin (vf t) . x implies $2 = ((f1 || H) . x) . $1 ) & ( $1 in (vf t) . x implies for r being SortSymbol of S st x = r holds
for q being Element of the Sorts of A . r st q = ((supp-term t) . r) . $1 holds
for u being ManySortedFunction of H, the Sorts of C st u = (f1 || H) +* (r,(supp-var t),v) holds
$2 = q value_at (C,u) ) ) ) );
A3: for y being object st y in H . x holds
ex z being object st S₂[y,z]

let y be object ; :: thesis:
assume y in H . x ; :: thesis:

per cases ;

suppose A4: ( p = r & y = t ) ; :: thesis:

take z = v; :: thesis:
thus S₂[y,z] by A4; :: thesis:

end;

suppose A5: ( ( p = r implies y <> t ) & y in (vf t) . x ) ; :: thesis:

then reconsider q = ((supp-term t) . p) . y as Element of the Sorts of A . p by FUNCT_2:5;
take z = q value_at (C,((f1 || H) +* (r,(supp-var t),v))); :: thesis:
thus S₂[y,z] by A5; :: thesis:

end;

suppose A6: ( ( p = r implies y <> t ) & y nin (vf t) . x ) ; :: thesis:

take z = ((f1 || H) . x) . y; :: thesis:
thus S₂[y,z] by A6; :: thesis:

end;

consider j being Function such that
A7: ( dom j = H . x & ( for y being object st y in H . x holds
S₂[y,j . y] ) ) from CLASSES1:sch 1(A3);
take j ; :: thesis:
thus S₁[x,j] :: thesis:

proof

take f = j; :: thesis:
thus ( f = j & dom f = H . x ) by A7; :: thesis:
thus ( x = r & t in H . r implies f . t = v ) by A7; :: thesis:
let r be SortSymbol of S; :: thesis:
assume A8: x = r ; :: thesis:
let x be Element of H . r; :: thesis:
assume A9: ( r = r implies x <> t ) ; :: thesis:
hence ( x nin (vf t) . r implies f . x = ((f1 || H) . r) . x ) by A7, A8; :: thesis:
thus ( x in (vf t) . r implies for q being Element of A,r st q = ((supp-term t) . r) . x holds
for u being ManySortedFunction of H, the Sorts of C st u = (f1 || H) +* (r,(supp-var t),v) holds
f . x = q value_at (C,u) ) by A8, A7, A9; :: thesis:

end;

consider k being Function such that
A10: ( dom k = the carrier of S & ( for x being object st x in the carrier of S holds
S₁[x,k . x] ) ) from CLASSES1:sch 1(A2);
reconsider k = k as ManySortedSet of the carrier of S by A10, RELAT_1:def 18, PARTFUN1:def 2;
k is Function-yielding

proof

let x be object ; :: according to FUNCOP_1:def 6 :: thesis:
assume x in dom k ; :: thesis:
then S₁[x,k . x] by A10;
hence k . x is set ; :: thesis:

end;

then reconsider k = k as ManySortedFunction of the carrier of S ;
k is ManySortedFunction of H, the Sorts of C

proof

let x be object ; :: according to PBOOLE:def 15 :: thesis:
assume x in the carrier of S ; :: thesis:
then reconsider p = x as SortSymbol of S ;
consider f being Function such that
A11: ( k . p = f & dom f = H . p & ( p = r & t in H . r implies f . t = v ) & ( for r being SortSymbol of S st p = r holds
for x being Element of H . r st ( r = r implies x <> t ) holds
( ( x nin (vf t) . r implies f . x = ((f1 || H) . r) . x ) & ( x in (vf t) . r implies for q being Element of A,r st q = ((supp-term t) . r) . x holds
for u being ManySortedFunction of H, the Sorts of C st u = (f1 || H) +* (r,(supp-var t),v) holds
f . x = q value_at (C,u) ) ) ) ) by A10;
rng f c= the Sorts of C . p

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f ; :: thesis:
then consider z being object such that
A12: ( z in dom f & y = f . z ) by FUNCT_1:def 3;

per cases ;

suppose A13: ( r = p & z = t ) ; :: thesis:

thus y in the Sorts of C . p by A11, A12, A13; :: thesis:

end;

suppose ( ( p = r implies t <> z ) & z nin (vf t) . p ) ; :: thesis:

then y = ((f1 || H) . p) . z by A11, A12;
hence y in the Sorts of C . p by A11, A12, FUNCT_2:5; :: thesis:

end;

suppose A14: ( ( p = r implies t <> z ) & z in (vf t) . p ) ; :: thesis:

vf t is ManySortedSubset of H by Th35;
then (vf t) . p c= H . p by PBOOLE:def 2, PBOOLE:def 18;
then reconsider z = z as Element of H . p by A14;
reconsider q = ((supp-term t) . p) . z as Element of the Sorts of A . p by A14, FUNCT_2:5;
reconsider u = (f1 || H) +* (r,(supp-var t),v) as ManySortedFunction of H, the Sorts of C ;
y = q value_at (C,u) by A12, A14, A11;
hence y in the Sorts of C . p ; :: thesis:

end;

hence k . x is Element of bool [:(H . x),( the Sorts of C . x):] by A11, FUNCT_2:2; :: thesis:

end;

then reconsider k = k as ManySortedFunction of H, the Sorts of C ;
consider h being ManySortedFunction of A,C such that
A15: ( h is_homomorphism A,C & k = h || I ) by MSAFREE4:46;
reconsider w = h || the generators of G as Element of C -States the generators of G by A15, Def18;
take w ; :: thesis:

hereby :: thesis:

per cases ;

suppose A16: t in H . r ; :: thesis:

A17: S₁[r,k . r] by A10;
thus (w . r) . t = ((h . r) | ( the generators of G . r)) . t by MSAFREE:def 1
.= (h . r) . t by Def21, FUNCT_1:49
.= ((h . r) | (H . r)) . t by A16, FUNCT_1:49
.= v by A17, A16, A15, MSAFREE:def 1 ; :: thesis:

end;

suppose A18: t nin H . r ; :: thesis:

A19: now :: thesis:

let a be SortSymbol of S; :: thesis:
A20: S₁[a,k . a] by A10;
let z be Element of (FreeGen X) . a; :: thesis:
( a = r implies t <> z ) by A18;
hence ( z in (vf t) . a implies for q being Element of A,a st q = ((supp-term t) . a) . z holds
(k . a) . z = q value_at (C,((f1 || H) +* (r,(supp-var t),v))) ) by A20; :: thesis:

end;

thus (w . r) . t = ((h . r) | ( the generators of G . r)) . t by MSAFREE:def 1
.= (h . r) . t by Def21, FUNCT_1:49
.= v by A15, A18, A19, A1 ; :: thesis:

end;

let p be SortSymbol of S; :: thesis:
let x be Element of (FreeGen X) . p; :: thesis:
assume A21: ( p = r implies x <> t ) ; :: thesis:
reconsider x0 = x as Element of H . p ;
consider f being Function such that
A22: ( f = k . p & dom f = H . p & ( p = r & t in H . r implies f . t = v ) & ( for r being SortSymbol of S st p = r holds
for x being Element of H . r st ( r = r implies x <> t ) holds
( ( x nin (vf t) . r implies f . x = ((f1 || H) . r) . x ) & ( x in (vf t) . r implies for q being Element of A,r st q = ((supp-term t) . r) . x holds
for u being ManySortedFunction of H, the Sorts of C st u = (f1 || H) +* (r,(supp-var t),v) holds
f . x = q value_at (C,u) ) ) ) ) by A10;
A23: ( x in H . p & H . p c= the generators of G . p ) by PBOOLE:def 2, PBOOLE:def 18;
A24: (w . p) . x = ((h . p) | ( the generators of G . p)) . x by MSAFREE:def 1
.= (h . p) . x by A23, FUNCT_1:49
.= ((h . p) | (I . p)) . x by FUNCT_1:49
.= (k . p) . x by A15, MSAFREE:def 1 ;
((f1 || H) . p) . x = ((f1 . p) | (H . p)) . x by MSAFREE:def 1
.= (s . p) . x by FUNCT_1:49 ;
hence ( x nin (vf t) . p implies (w . p) . x = (s . p) . x ) by A21, A22, A24; :: thesis:
let u be ManySortedFunction of FreeGen X, the Sorts of C; :: thesis:
let H be ManySortedSubset of the generators of G; :: thesis:
assume A25: H = FreeGen X ; :: thesis:
let f be ManySortedFunction of the generators of G, the Sorts of C; :: thesis:
assume A26: ( f = s & u = (f || H) +* (r,(supp-var t),v) ) ; :: thesis:
assume A27: x in (vf t) . p ; :: thesis:
let q be Element of A,p; :: thesis:
assume q = ((supp-term t) . p) . x ; :: thesis:
hence (w . p) . x = q value_at (C,u) by A21, A24, A22, A25, A26, A27; :: thesis: