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