let f, g be XFinSequence-yielding Function; :: thesis: ( dom f = dom p & ( for x being set st x in dom p holds
f . x = s ^ (p . x) ) & dom g = dom p & ( for x being set st x in dom p holds
g . x = s ^ (p . x) ) implies f = g )
assume that
A4: ( dom f = dom p & ( for x being set st x in dom p holds
f . x = s ^ (p . x) ) ) and
A5: ( dom g = dom p & ( for x being set st x in dom p holds
g . x = s ^ (p . x) ) ) ; :: 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 = s ^ (p . x) & g . x = s ^ (p . x) ) by A4, A5;
hence f . x = g . x ; :: thesis: verum

end;

hence f = g by A4, A5, FUNCT_1:9; :: thesis: verum