let f1, f2 be Function of (TOP-REAL 2),R^1; ( ( 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 that
A4:
for p being Point of (TOP-REAL 2) holds f1 . p = tricord3 (p1,p2,p3,p)
and
A5:
for p being Point of (TOP-REAL 2) holds f2 . p = tricord3 (p1,p2,p3,p)
; f1 = f2
A6:
for x being object st x in dom f1 holds
f1 . x = f2 . x
dom f1 = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
then
dom f1 = dom f2
by FUNCT_2:def 1;
hence
f1 = f2
by A6, FUNCT_1:2; verum