defpred S_{1}[ object , object ] means for x being set st x = $1 holds

$2 = (p . x) ^ s;

A8: for x being object st x in dom p holds

ex y being object st S_{1}[x,y]

A9: ( dom f = dom p & ( for x being object st x in dom p holds

S_{1}[x,f . x] ) )
from CLASSES1:sch 1(A8);

take g ; :: thesis: ( dom g = dom p & ( for x being set st x in dom p holds

g . x = (p . x) ^ s ) )

thus ( dom g = dom p & ( for x being set st x in dom p holds

g . x = (p . x) ^ s ) ) by A9; :: thesis: verum

$2 = (p . x) ^ s;

A8: for x being object st x in dom p holds

ex y being object st S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in dom p implies ex y being object st S_{1}[x,y] )

assume x in dom p ; :: thesis: ex y being object st S_{1}[x,y]

take (p . x) ^ s ; :: thesis: S_{1}[x,(p . x) ^ s]

thus S_{1}[x,(p . x) ^ s]
; :: thesis: verum

end;assume x in dom p ; :: thesis: ex y being object st S

take (p . x) ^ s ; :: thesis: S

thus S

A9: ( dom f = dom p & ( for x being object st x in dom p holds

S

now :: thesis: for x being set st x in dom f holds

f . x is XFinSequence

then reconsider g = f as XFinSequence-yielding Function by Def1;f . x is XFinSequence

let x be set ; :: thesis: ( x in dom f implies f . x is XFinSequence )

assume x in dom f ; :: thesis: f . x is XFinSequence

then f . x = (p . x) ^ s by A9;

hence f . x is XFinSequence ; :: thesis: verum

end;assume x in dom f ; :: thesis: f . x is XFinSequence

then f . x = (p . x) ^ s by A9;

hence f . x is XFinSequence ; :: thesis: verum

take g ; :: thesis: ( dom g = dom p & ( for x being set st x in dom p holds

g . x = (p . x) ^ s ) )

thus ( dom g = dom p & ( for x being set st x in dom p holds

g . x = (p . x) ^ s ) ) by A9; :: thesis: verum