let f1, f2 be Function of (TOP-REAL 2),R^1 ; :: thesis: ( ( for p being Point of (TOP-REAL 2) holds f1 . p = tricord3 p1,p2,p3,p ) & ( for p being Point of (TOP-REAL 2) holds f2 . p = tricord3 p1,p2,p3,p ) implies f1 = f2 )
assume A3: ( ( for p being Point of (TOP-REAL 2) holds f1 . p = tricord3 p1,p2,p3,p ) & ( for p being Point of (TOP-REAL 2) holds f2 . p = tricord3 p1,p2,p3,p ) ) ; :: thesis: f1 = f2
dom f1 = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A4: dom f1 = dom f2 by FUNCT_2:def 1;
for x being set st x in dom f1 holds
f1 . x = f2 . x

proof

let x be set ; :: thesis: ( x in dom f1 implies f1 . x = f2 . x )
assume x in dom f1 ; :: thesis: f1 . x = f2 . x
then reconsider p0 = x as Point of (TOP-REAL 2) by FUNCT_2:def 1;
f1 . p0 = tricord3 p1,p2,p3,p0 by A3;
hence f1 . x = f2 . x by A3; :: thesis: verum

end;

hence f1 = f2 by A4, FUNCT_1:9; :: thesis: verum