let p1, p2 be Function; :: thesis: ( dom p1 = dom f & ( for x being object st x in dom f holds
p1 . x = (f . x) `2 ) & dom p2 = dom f & ( for x being object st x in dom f holds
p2 . x = (f . x) `2 ) implies p1 = p2 )
assume that
A6: dom p1 = dom f and
A7: for x being object st x in dom f holds
p1 . x = (f . x) `2 and
A8: dom p2 = dom f and
A9: for x being object st x in dom f holds
p2 . x = (f . x) `2 ; :: thesis: p1 = p2

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

let x be object ; :: thesis: ( x in dom f implies p1 . x = p2 . x )
assume A10: x in dom f ; :: thesis: p1 . x = p2 . x
then p1 . x = (f . x) `2 by A7;
hence p1 . x = p2 . x by A9, A10; :: thesis: verum

end;

hence p1 = p2 by A6, A8, FUNCT_1:2; :: thesis: verum