defpred S₁[ 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₁[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 s ^ (p . x) ; :: thesis: S₁[x,s ^ (p . x)]
thus S₁[x,s ^ (p . x)] ; :: thesis: verum

end;

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

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