defpred S₁[ Element of REAL , Element of REAL , set ] means ex c being Element of REAL 2 st
( c = $3 & $3 = <*$1,$2*> );
A1: for x, y being Element of REAL ex u being Element of REAL 2 st S₁[x,y,u]

proof

let x, y be Element of REAL ; :: thesis: ex u being Element of REAL 2 st S₁[x,y,u]
take <*x,y*> ; :: thesis: ( <*x,y*> is Element of bool [:NAT ,REAL :] & <*x,y*> is FinSequence of REAL & <*x,y*> is Element of REAL 2 & S₁[x,y,<*x,y*>] )
<*x,y*> is Element of REAL 2 by CATALG_1:10;
hence ( <*x,y*> is Element of bool [:NAT ,REAL :] & <*x,y*> is FinSequence of REAL & <*x,y*> is Element of REAL 2 & S₁[x,y,<*x,y*>] ) ; :: thesis: verum

end;

consider f being Function of [:REAL ,REAL :],(REAL 2) such that
A2: for x, y being Element of REAL holds S₁[x,y,f . x,y] from BINOP_1:sch 3(A1);
( the carrier of [:R^1 ,R^1 :] = [:the carrier of R^1 ,the carrier of R^1 :] & the carrier of R^1 = REAL & the carrier of (TOP-REAL 2) = REAL 2 ) by BORSUK_1:def 5, TOPMETR:24, EUCLID:25;
then reconsider f = f as Function of [:R^1 ,R^1 :],(TOP-REAL 2) ;
take f ; :: thesis: for x, y being Real holds f . [x,y] = <*x,y*>
for x, y being Real holds f . [x,y] = <*x,y*>

proof

let x, y be Real; :: thesis: f . [x,y] = <*x,y*>
S₁[x,y,f . x,y] by A2;
hence f . [x,y] = <*x,y*> ; :: thesis: verum

end;

hence for x, y being Real holds f . [x,y] = <*x,y*> ; :: thesis: verum