let f, g be Function of [:R^1 ,R^1 :],(TOP-REAL 2); :: thesis: ( ( for x, y being real number holds f . [x,y] = <*x,y*> ) & ( for x, y being real number holds g . [x,y] = <*x,y*> ) implies f = g )
assume that
A2: for x, y being real number holds f . [x,y] = <*x,y*> and
A3: for x, y being real number holds g . [x,y] = <*x,y*> ; :: thesis: f = g

now

let a be Point of [:R^1 ,R^1 :]; :: thesis: f . a = g . a
consider x, y being Element of the carrier of R^1 such that
A4: a = [x,y] by Lm1, DOMAIN_1:9;
thus f . a = <*x,y*> by A2, A4
.= g . a by A3, A4 ; :: thesis: verum

end;

hence f = g by FUNCT_2:113; :: thesis: verum