defpred S₁[ 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₁[x,y]

proof

let x be object ; :: thesis: ( x in dom p implies ex y being object st S₁[x,y] )
assume x in dom p ; :: thesis: ex y being object st S₁[x,y]
take (p . x) ^ s ; :: thesis: S₁[x,(p . x) ^ s]
thus S₁[x,(p . x) ^ s] ; :: thesis: verum

end;

consider f being Function such that
A9: ( dom f = dom p & ( for x being object st x in dom p holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A8);

now :: thesis: for x being set st x in dom f holds
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;

then reconsider g = f as XFinSequence-yielding Function by Def1;
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