defpred S1[ 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 S1[x,y,u]
proof
let x,
y be
Element of
REAL ;
ex u being Element of REAL 2 st S1[x,y,u]
take
<*x,y*>
;
( <*x,y*> is Element of bool [:NAT,REAL:] & <*x,y*> is FinSequence of REAL & <*x,y*> is Element of REAL 2 & S1[x,y,<*x,y*>] )
<*x,y*> is
Element of
REAL 2
by FINSEQ_2:137;
hence
(
<*x,y*> is
Element of
bool [:NAT,REAL:] &
<*x,y*> is
FinSequence of
REAL &
<*x,y*> is
Element of
REAL 2 &
S1[
x,
y,
<*x,y*>] )
;
verum
end;
consider f being Function of [:REAL,REAL:],(REAL 2) such that
A2:
for x, y being Element of REAL holds S1[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:]
by BORSUK_1:def 2;
then reconsider f = f as Function of [:R^1,R^1:],(TOP-REAL 2) by EUCLID:22, TOPMETR:17;
take
f
; for x, y being Real holds f . [x,y] = <*x,y*>
for x, y being Real holds f . [x,y] = <*x,y*>
hence
for x, y being Real holds f . [x,y] = <*x,y*>
; verum