let f, g be Function of [:R^1,R^1:],(TOP-REAL 2); :: thesis: ( ( 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*> ; :: thesis: f = g
let a be Point of [:R^1,R^1:]; :: according to FUNCT_2:def 8 :: thesis: 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 ; :: thesis: verum