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

A3: dom f = dom p and

A4: for x being set st x in dom p holds

f . x = s ^ (p . x) and

A5: dom g = dom p and

A6: for x being set st x in dom p holds

g . x = s ^ (p . x) ; :: thesis: f = g

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

A3: dom f = dom p and

A4: for x being set st x in dom p holds

f . x = s ^ (p . x) and

A5: dom g = dom p and

A6: for x being set st x in dom p holds

g . x = s ^ (p . x) ; :: thesis: f = g

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

f . x = g . x

hence
f = g
by A3, A5, FUNCT_1:2; :: thesis: verumf . x = g . x

let x be object ; :: thesis: ( x in dom f implies f . x = g . x )

assume A7: x in dom f ; :: thesis: f . x = g . x

then f . x = s ^ (p . x) by A3, A4;

hence f . x = g . x by A3, A6, A7; :: thesis: verum

end;assume A7: x in dom f ; :: thesis: f . x = g . x

then f . x = s ^ (p . x) by A3, A4;

hence f . x = g . x by A3, A6, A7; :: thesis: verum