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
A10: dom f = dom p and
A11: for x being set st x in dom p holds
f . x = (p . x) ^ s and
A12: dom g = dom p and
A13: for x being set st x in dom p holds
g . x = (p . x) ^ s ; :: thesis: f = g

now :: thesis: for x being object st x in dom f holds
f . x = g . x

let x be object ; :: thesis: ( x in dom f implies f . x = g . x )
assume A14: x in dom f ; :: thesis: f . x = g . x
then f . x = (p . x) ^ s by A10, A11;
hence f . x = g . x by A10, A13, A14; :: thesis: verum

end;

hence f = g by A10, A12, FUNCT_1:2; :: thesis: verum