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

$2 = s ^ (p . x);

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

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

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

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

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

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

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

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

$2 = s ^ (p . x);

A1: 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 s ^ (p . x) ; :: thesis: S_{1}[x,s ^ (p . x)]

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

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

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

thus S

A2: ( 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 = s ^ (p . x) by A2;

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

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

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

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 = s ^ (p . x) ) )

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

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