defpred S1[ 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 S1[x,y]
proof
let x be object ; :: thesis: ( x in dom p implies ex y being object st S1[x,y] )
assume x in dom p ; :: thesis: ex y being object st S1[x,y]
take s ^ (p . x) ; :: thesis: S1[x,s ^ (p . x)]
thus S1[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
S1[x,f . x] ) ) from
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