consider f being Function of [:R^1 ,R^1 :],(TOP-REAL 2) such that
A1: for x, y being Real holds f . [x,y] = <*x,y*> by BORSUK_6:24;
take f ; :: thesis: for x, y being real number holds f . [x,y] = <*x,y*>
let x, y be real number ; :: thesis: f . [x,y] = <*x,y*>
( x is Real & y is Real ) by XREAL_0:def 1;
hence f . [x,y] = <*x,y*> by A1; :: thesis: verum