let p1, p2 be Function; :: thesis: ( dom p1 = dom f & ( for x being object st x in dom f holds
p1 . x = (f . x) `1 ) & dom p2 = dom f & ( for x being object st x in dom f holds
p2 . x = (f . x) `1 ) implies p1 = p2 )
assume that
A1: dom p1 = dom f and
A2: for x being object st x in dom f holds
p1 . x = (f . x) `1 and
A3: dom p2 = dom f and
A4: for x being object st x in dom f holds
p2 . x = (f . x) `1 ; :: 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 A5: x in dom f ; :: thesis: p1 . x = p2 . x
then p1 . x = (f . x) `1 by A2;
hence p1 . x = p2 . x by A4, A5; :: thesis: verum

end;

hence p1 = p2 by A1, A3, FUNCT_1:2; :: thesis: verum