let f, g be Function of [:R^1,R^1:],(TOP-REAL 2); ( ( for x, y being Real holds f . [x,y] = <*x,y*> ) & ( for x, y being Real holds g . [x,y] = <*x,y*> ) implies f = g )
assume that
A1:
for x, y being Real holds f . [x,y] = <*x,y*>
and
A2:
for x, y being Real holds g . [x,y] = <*x,y*>
; f = g
let a be Point of [:R^1,R^1:]; FUNCT_2:def 8 f . a = g . a
consider x, y being Element of the carrier of R^1 such that
A3:
a = [x,y]
by Lm1, DOMAIN_1:1;
thus f . a =
<*x,y*>
by A1, A3
.=
g . a
by A2, A3
; verum