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_{1}[ 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_{1}[x,y]

A10: ( dom k = the carrier of S & ( for x being object st x in the carrier of S holds

S_{1}[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

k is 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: ( (w . r) . t = v & ( for p being SortSymbol of S

for x being Element of (FreeGen X) . p st ( p = r implies x <> t ) holds

( ( x nin (vf t) . p implies (w . p) . x = (s . p) . x ) & ( for u being ManySortedFunction of FreeGen X, the Sorts of C

for H being ManySortedSubset of the generators of G st H = FreeGen X holds

for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(w . p) . x = q value_at (C,u) ) ) ) )

( ( x nin (vf t) . p implies (w . p) . x = (s . p) . x ) & ( for u being ManySortedFunction of FreeGen X, the Sorts of C

for H being ManySortedSubset of the generators of G st H = FreeGen X holds

for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(w . p) . x = q value_at (C,u) ) )

let x be Element of (FreeGen X) . p; :: thesis: ( ( p = r implies x <> t ) implies ( ( x nin (vf t) . p implies (w . p) . x = (s . p) . x ) & ( for u being ManySortedFunction of FreeGen X, the Sorts of C

for H being ManySortedSubset of the generators of G st H = FreeGen X holds

for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(w . p) . x = q value_at (C,u) ) ) )

assume A21: ( p = r implies x <> t ) ; :: thesis: ( ( x nin (vf t) . p implies (w . p) . x = (s . p) . x ) & ( for u being ManySortedFunction of FreeGen X, the Sorts of C

for H being ManySortedSubset of the generators of G st H = FreeGen X holds

for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(w . p) . x = q value_at (C,u) ) )

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: for u being ManySortedFunction of FreeGen X, the Sorts of C

for H being ManySortedSubset of the generators of G st H = FreeGen X holds

for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(w . p) . x = q value_at (C,u)

let u be ManySortedFunction of FreeGen X, the Sorts of C; :: thesis: for H being ManySortedSubset of the generators of G st H = FreeGen X holds

for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(w . p) . x = q value_at (C,u)

let H be ManySortedSubset of the generators of G; :: thesis: ( H = FreeGen X implies for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(w . p) . x = q value_at (C,u) )

assume A25: H = FreeGen X ; :: thesis: for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(w . p) . x = q value_at (C,u)

let f be ManySortedFunction of the generators of G, the Sorts of C; :: thesis: ( f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p implies for q being Element of A,p st q = ((supp-term t) . p) . x holds

(w . p) . x = q value_at (C,u) )

assume A26: ( f = s & u = (f || H) +* (r,(supp-var t),v) ) ; :: thesis: ( not x in (vf t) . p or for q being Element of A,p st q = ((supp-term t) . p) . x holds

(w . p) . x = q value_at (C,u) )

assume A27: x in (vf t) . p ; :: thesis: for q being Element of A,p st q = ((supp-term t) . p) . x holds

(w . p) . x = q value_at (C,u)

let q be Element of A,p; :: thesis: ( q = ((supp-term t) . p) . x implies (w . p) . x = q value_at (C,u) )

assume q = ((supp-term t) . p) . x ; :: thesis: (w . p) . x = q value_at (C,u)

hence (w . p) . x = q value_at (C,u) by A21, A24, A22, A25, A26, A27; :: thesis: verum

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

( 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

proof

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

assume x in the carrier of S ; :: thesis: ex y being object st S_{1}[x,y]

then reconsider p = x as SortSymbol of S ;

defpred S_{2}[ 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_{2}[y,z]

A7: ( dom j = H . x & ( for y being object st y in H . x holds

S_{2}[y,j . y] ) )
from CLASSES1:sch 1(A3);

take j ; :: thesis: S_{1}[x,j]

thus S_{1}[x,j]
:: thesis: verum

end;assume x in the carrier of S ; :: thesis: ex y being object st S

then reconsider p = x as SortSymbol of S ;

defpred S

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

proof

consider j being Function such that
let y be object ; :: thesis: ( y in H . x implies ex z being object st S_{2}[y,z] )

assume y in H . x ; :: thesis: ex z being object st S_{2}[y,z]

end;assume y in H . x ; :: thesis: ex z being object st S

per cases
( ( p = r & y = t ) or ( ( p = r implies y <> t ) & y in (vf t) . x ) or ( ( p = r implies y <> t ) & y nin (vf t) . x ) )
;

end;

suppose A5:
( ( p = r implies y <> t ) & y in (vf t) . x )
; :: thesis: ex z being object st S_{2}[y,z]

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: S_{2}[y,z]

thus S_{2}[y,z]
by A5; :: thesis: verum

end;take z = q value_at (C,((f1 || H) +* (r,(supp-var t),v))); :: thesis: S

thus S

A7: ( dom j = H . x & ( for y being object st y in H . x holds

S

take j ; :: thesis: S

thus S

proof

take f = j; :: thesis: ( f = j & dom f = H . x & ( x = r & t in H . r implies f . t = v ) & ( for r being SortSymbol of S st x = 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) ) ) ) )

thus ( f = j & dom f = H . x ) by A7; :: thesis: ( ( x = r & t in H . r implies f . t = v ) & ( for r being SortSymbol of S st x = 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) ) ) ) )

thus ( x = r & t in H . r implies f . t = v ) by A7; :: thesis: for r being SortSymbol of S st x = 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) ) )

let r be SortSymbol of S; :: thesis: ( x = r implies 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) ) ) )

assume A8: x = r ; :: thesis: 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) ) )

let x be Element of H . r; :: thesis: ( ( r = r implies x <> t ) implies ( ( 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) ) ) )

assume A9: ( r = r implies x <> t ) ; :: thesis: ( ( 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) ) )

hence ( x nin (vf t) . r implies f . x = ((f1 || H) . r) . x ) by A7, A8; :: thesis: ( 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) )

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: verum

end;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) ) ) ) )

thus ( f = j & dom f = H . x ) by A7; :: thesis: ( ( x = r & t in H . r implies f . t = v ) & ( for r being SortSymbol of S st x = 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) ) ) ) )

thus ( x = r & t in H . r implies f . t = v ) by A7; :: thesis: for r being SortSymbol of S st x = 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) ) )

let r be SortSymbol of S; :: thesis: ( x = r implies 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) ) ) )

assume A8: x = r ; :: thesis: 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) ) )

let x be Element of H . r; :: thesis: ( ( r = r implies x <> t ) implies ( ( 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) ) ) )

assume A9: ( r = r implies x <> t ) ; :: thesis: ( ( 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) ) )

hence ( x nin (vf t) . r implies f . x = ((f1 || H) . r) . x ) by A7, A8; :: thesis: ( 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) )

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: verum

A10: ( dom k = the carrier of S & ( for x being object st x in the carrier of S holds

S

reconsider k = k as ManySortedSet of the carrier of S by A10, RELAT_1:def 18, PARTFUN1:def 2;

k is Function-yielding

proof

then reconsider k = k as ManySortedFunction of the carrier of S ;
let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 k or k . x is set )

assume x in dom k ; :: thesis: k . x is set

then S_{1}[x,k . x]
by A10;

hence k . x is set ; :: thesis: verum

end;assume x in dom k ; :: thesis: k . x is set

then S

hence k . x is set ; :: thesis: verum

k is ManySortedFunction of H, the Sorts of C

proof

then reconsider k = k as ManySortedFunction of H, the Sorts of C ;
let x be object ; :: according to PBOOLE:def 15 :: thesis: ( not x in the carrier of S or k . x is Element of bool [:(H . x),( the Sorts of C . x):] )

assume x in the carrier of S ; :: thesis: k . x is Element of bool [:(H . x),( the Sorts of C . x):]

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

end;assume x in the carrier of S ; :: thesis: k . x is Element of bool [:(H . x),( the Sorts of C . x):]

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

hence
k . x is Element of bool [:(H . x),( the Sorts of C . x):]
by A11, FUNCT_2:2; :: thesis: verum
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in the Sorts of C . p )

assume y in rng f ; :: thesis: y in the Sorts of C . p

then consider z being object such that

A12: ( z in dom f & y = f . z ) by FUNCT_1:def 3;

end;assume y in rng f ; :: thesis: y in the Sorts of C . p

then consider z being object such that

A12: ( z in dom f & y = f . z ) by FUNCT_1:def 3;

per cases
( ( r = p & z = t ) or ( ( p = r implies t <> z ) & z nin (vf t) . p ) or ( ( p = r implies t <> z ) & z in (vf t) . p ) )
;

end;

suppose
( ( p = r implies t <> z ) & z nin (vf t) . p )
; :: thesis: y in the Sorts of C . p

then
y = ((f1 || H) . p) . z
by A11, A12;

hence y in the Sorts of C . p by A11, A12, FUNCT_2:5; :: thesis: verum

end;hence y in the Sorts of C . p by A11, A12, FUNCT_2:5; :: thesis: verum

suppose A14:
( ( p = r implies t <> z ) & z in (vf t) . p )
; :: thesis: y in the Sorts of C . p

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: verum

end;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: verum

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: ( (w . r) . t = v & ( for p being SortSymbol of S

for x being Element of (FreeGen X) . p st ( p = r implies x <> t ) holds

( ( x nin (vf t) . p implies (w . p) . x = (s . p) . x ) & ( for u being ManySortedFunction of FreeGen X, the Sorts of C

for H being ManySortedSubset of the generators of G st H = FreeGen X holds

for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(w . p) . x = q value_at (C,u) ) ) ) )

hereby :: thesis: for p being SortSymbol of S

for x being Element of (FreeGen X) . p st ( p = r implies x <> t ) holds

( ( x nin (vf t) . p implies (w . p) . x = (s . p) . x ) & ( for u being ManySortedFunction of FreeGen X, the Sorts of C

for H being ManySortedSubset of the generators of G st H = FreeGen X holds

for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(w . p) . x = q value_at (C,u) ) )
end;

let p be SortSymbol of S; :: thesis: for x being Element of (FreeGen X) . p st ( p = r implies x <> t ) holds for x being Element of (FreeGen X) . p st ( p = r implies x <> t ) holds

( ( x nin (vf t) . p implies (w . p) . x = (s . p) . x ) & ( for u being ManySortedFunction of FreeGen X, the Sorts of C

for H being ManySortedSubset of the generators of G st H = FreeGen X holds

for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(w . p) . x = q value_at (C,u) ) )

per cases
( t in H . r or t nin H . r )
;

end;

suppose A16:
t in H . r
; :: thesis: (w . r) . t = v

A17:
S_{1}[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: verum

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

.= ((h . r) | (H . r)) . t by A16, FUNCT_1:49

.= v by A17, A16, A15, MSAFREE:def 1 ; :: thesis: verum

suppose A18:
t nin H . r
; :: thesis: (w . r) . t = v

.= (h . r) . t by Def21, FUNCT_1:49

.= v by A15, A18, A19, A1 ; :: thesis: verum

end;

A19: now :: thesis: for a being SortSymbol of S

for z being Element of (FreeGen X) . a st z in (vf t) . a holds

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)))

thus (w . r) . t =
((h . r) | ( the generators of G . r)) . t
by MSAFREE:def 1
for z being Element of (FreeGen X) . a st z in (vf t) . a holds

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)))

let a be SortSymbol of S; :: thesis: for z being Element of (FreeGen X) . a st z in (vf t) . a holds

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)))

A20: S_{1}[a,k . a]
by A10;

let z be Element of (FreeGen X) . a; :: thesis: ( 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))) )

( 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: verum

end;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)))

A20: S

let z be Element of (FreeGen X) . a; :: thesis: ( 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))) )

( 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: verum

.= (h . r) . t by Def21, FUNCT_1:49

.= v by A15, A18, A19, A1 ; :: thesis: verum

( ( x nin (vf t) . p implies (w . p) . x = (s . p) . x ) & ( for u being ManySortedFunction of FreeGen X, the Sorts of C

for H being ManySortedSubset of the generators of G st H = FreeGen X holds

for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(w . p) . x = q value_at (C,u) ) )

let x be Element of (FreeGen X) . p; :: thesis: ( ( p = r implies x <> t ) implies ( ( x nin (vf t) . p implies (w . p) . x = (s . p) . x ) & ( for u being ManySortedFunction of FreeGen X, the Sorts of C

for H being ManySortedSubset of the generators of G st H = FreeGen X holds

for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(w . p) . x = q value_at (C,u) ) ) )

assume A21: ( p = r implies x <> t ) ; :: thesis: ( ( x nin (vf t) . p implies (w . p) . x = (s . p) . x ) & ( for u being ManySortedFunction of FreeGen X, the Sorts of C

for H being ManySortedSubset of the generators of G st H = FreeGen X holds

for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(w . p) . x = q value_at (C,u) ) )

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: for u being ManySortedFunction of FreeGen X, the Sorts of C

for H being ManySortedSubset of the generators of G st H = FreeGen X holds

for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(w . p) . x = q value_at (C,u)

let u be ManySortedFunction of FreeGen X, the Sorts of C; :: thesis: for H being ManySortedSubset of the generators of G st H = FreeGen X holds

for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(w . p) . x = q value_at (C,u)

let H be ManySortedSubset of the generators of G; :: thesis: ( H = FreeGen X implies for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(w . p) . x = q value_at (C,u) )

assume A25: H = FreeGen X ; :: thesis: for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(w . p) . x = q value_at (C,u)

let f be ManySortedFunction of the generators of G, the Sorts of C; :: thesis: ( f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p implies for q being Element of A,p st q = ((supp-term t) . p) . x holds

(w . p) . x = q value_at (C,u) )

assume A26: ( f = s & u = (f || H) +* (r,(supp-var t),v) ) ; :: thesis: ( not x in (vf t) . p or for q being Element of A,p st q = ((supp-term t) . p) . x holds

(w . p) . x = q value_at (C,u) )

assume A27: x in (vf t) . p ; :: thesis: for q being Element of A,p st q = ((supp-term t) . p) . x holds

(w . p) . x = q value_at (C,u)

let q be Element of A,p; :: thesis: ( q = ((supp-term t) . p) . x implies (w . p) . x = q value_at (C,u) )

assume q = ((supp-term t) . p) . x ; :: thesis: (w . p) . x = q value_at (C,u)

hence (w . p) . x = q value_at (C,u) by A21, A24, A22, A25, A26, A27; :: thesis: verum