let f, g be XFinSequence-yielding Function; :: thesis: ( dom f = dom p & ( for x being set st x in dom p holds
f . x = (p . x) ^ s ) & dom g = dom p & ( for x being set st x in dom p holds
g . x = (p . x) ^ s ) implies f = g )
assume that
A9: ( dom f = dom p & ( for x being set st x in dom p holds
f . x = (p . x) ^ s ) ) and
A10: ( dom g = dom p & ( for x being set st x in dom p holds
g . x = (p . x) ^ s ) ) ; :: thesis: f = g

now

let x be set ; :: thesis: ( x in dom f implies f . x = g . x )
assume x in dom f ; :: thesis: f . x = g . x
then ( f . x = (p . x) ^ s & g . x = (p . x) ^ s ) by A9, A10;
hence f . x = g . x ; :: thesis: verum

end;

hence f = g by A9, A10, FUNCT_1:9; :: thesis: verum