let f1, f2 be Function of (TOP-REAL 2),R^1; :: thesis: ( ( for p being Point of (TOP-REAL 2) holds f1 . p = tricord2 (p1,p2,p3,p) ) & ( for p being Point of (TOP-REAL 2) holds f2 . p = tricord2 (p1,p2,p3,p) ) implies f1 = f2 )

assume that

A3: for p being Point of (TOP-REAL 2) holds f1 . p = tricord2 (p1,p2,p3,p) and

A4: for p being Point of (TOP-REAL 2) holds f2 . p = tricord2 (p1,p2,p3,p) ; :: thesis: f1 = f2

A5: for x being object st x in dom f1 holds

f1 . x = f2 . x

then dom f1 = dom f2 by FUNCT_2:def 1;

hence f1 = f2 by A5, FUNCT_1:2; :: thesis: verum

assume that

A3: for p being Point of (TOP-REAL 2) holds f1 . p = tricord2 (p1,p2,p3,p) and

A4: for p being Point of (TOP-REAL 2) holds f2 . p = tricord2 (p1,p2,p3,p) ; :: thesis: f1 = f2

A5: for x being object st x in dom f1 holds

f1 . x = f2 . x

proof

dom f1 = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
let x be object ; :: 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 = tricord2 (p1,p2,p3,p0) by A3;

hence f1 . x = f2 . x by A4; :: thesis: verum

end;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 = tricord2 (p1,p2,p3,p0) by A3;

hence f1 . x = f2 . x by A4; :: thesis: verum

then dom f1 = dom f2 by FUNCT_2:def 1;

hence f1 = f2 by A5, FUNCT_1:2; :: thesis: verum