let m, n be non zero Element of NAT ; :: thesis: ex f being Function of [:(REAL m),(REAL n):],(REAL (m + n)) st
( ( for x being Element of REAL m
for y being Element of REAL n holds f . (x,y) = x ^ y ) & f is one-to-one & f is onto )
defpred S₁[ object , object , object ] means ex x being Element of REAL m ex y being Element of REAL n st
( x = $1 & y = $2 & $3 = x ^ y );
A1: for x, y being object st x in REAL m & y in REAL n holds
ex z being object st
( z in REAL (m + n) & S₁[x,y,z] )

proof

let x, y be object ; :: thesis: ( x in REAL m & y in REAL n implies ex z being object st
( z in REAL (m + n) & S₁[x,y,z] ) )
assume A2: ( x in REAL m & y in REAL n ) ; :: thesis: ex z being object st
( z in REAL (m + n) & S₁[x,y,z] )
then reconsider x0 = x as Element of REAL m ;
reconsider y0 = y as Element of REAL n by A2;
set z0 = x0 ^ y0;
A4: len (x0 ^ y0) = m + n by CARD_1:def 7;
x0 ^ y0 in REAL * by FINSEQ_1:def 11;
then x0 ^ y0 in (m + n) -tuples_on REAL by A4;
then reconsider z = x0 ^ y0 as Element of REAL (m + n) ;
take z ; :: thesis: ( z in REAL (m + n) & S₁[x,y,z] )
thus ( z in REAL (m + n) & S₁[x,y,z] ) ; :: thesis: verum

end;

consider f being Function of [:(REAL m),(REAL n):],(REAL (m + n)) such that
A5: for x, y being object st x in REAL m & y in REAL n holds
S₁[x,y,f . (x,y)] from BINOP_1:sch 1(A1);
take f ; :: thesis: ( ( for x being Element of REAL m
for y being Element of REAL n holds f . (x,y) = x ^ y ) & f is one-to-one & f is onto )
thus A6: for x being Element of REAL m
for y being Element of REAL n holds f . (x,y) = x ^ y :: thesis: ( f is one-to-one & f is onto )

proof

let x be Element of REAL m; :: thesis: for y being Element of REAL n holds f . (x,y) = x ^ y
let y be Element of REAL n; :: thesis: f . (x,y) = x ^ y
ex x0 being Element of REAL m ex y0 being Element of REAL n st
( x0 = x & y0 = y & f . (x,y) = x0 ^ y0 ) by A5;
hence f . (x,y) = x ^ y ; :: thesis: verum

end;

now :: thesis: for z1, z2 being object st z1 in [:(REAL m),(REAL n):] & z2 in [:(REAL m),(REAL n):] & f . z1 = f . z2 holds
z1 = z2

let z1, z2 be object ; :: thesis: ( z1 in [:(REAL m),(REAL n):] & z2 in [:(REAL m),(REAL n):] & f . z1 = f . z2 implies z1 = z2 )
assume A7: ( z1 in [:(REAL m),(REAL n):] & z2 in [:(REAL m),(REAL n):] & f . z1 = f . z2 ) ; :: thesis: z1 = z2
then consider x1, y1 being object such that
A8: ( x1 in REAL m & y1 in REAL n & z1 = [x1,y1] ) by ZFMISC_1:def 2;
consider x2, y2 being object such that
A9: ( x2 in REAL m & y2 in REAL n & z2 = [x2,y2] ) by A7, ZFMISC_1:def 2;
consider xx1 being Element of REAL m, yy1 being Element of REAL n such that
A10: ( xx1 = x1 & yy1 = y1 & f . (x1,y1) = xx1 ^ yy1 ) by A5, A8;
consider xx2 being Element of REAL m, yy2 being Element of REAL n such that
A11: ( xx2 = x2 & yy2 = y2 & f . (x2,y2) = xx2 ^ yy2 ) by A5, A9;
len xx1 = m by CARD_1:def 7
.= len xx2 by CARD_1:def 7 ;
then A12: dom xx1 = dom xx2 by FINSEQ_3:29;
xx1 = (xx1 ^ yy1) | (dom xx1) by FINSEQ_1:21
.= xx2 by A7, A8, A9, A10, A11, A12, FINSEQ_1:21 ;
hence z1 = z2 by A7, A8, A9, A10, A11, FINSEQ_1:33; :: thesis: verum

end;

hence f is one-to-one by FUNCT_2:19; :: thesis: f is onto

now :: thesis: for w being object st w in REAL (m + n) holds
w in rng f

let w be object ; :: thesis: ( w in REAL (m + n) implies w in rng f )
assume w in REAL (m + n) ; :: thesis: w in rng f
then A13: ex s being Element of REAL * st
( w = s & len s = m + n ) ;
then reconsider w0 = w as FinSequence of REAL ;
set x = w0 | m;
set y = w0 /^ m;
m <= m + n by NAT_1:11;
then A16: len (w0 /^ m) = (m + n) - m by A13, RFINSEQ:def 1;
A15: len (w0 | m) = m by A13, NAT_1:11, FINSEQ_1:59;
w0 | m in REAL * by FINSEQ_1:def 11;
then w0 | m in { s where s is Element of REAL * : len s = m } by A15;
then reconsider x0 = w0 | m as Element of REAL m ;
w0 /^ m in REAL * by FINSEQ_1:def 11;
then w0 /^ m in { s where s is Element of REAL * : len s = n } by A16;
then reconsider y0 = w0 /^ m as Element of REAL n ;
set z = [x0,y0];
A17: [x0,y0] in [:(REAL m),(REAL n):] by ZFMISC_1:87;
f . [x0,y0] = f . (x0,y0)
.= x0 ^ y0 by A6
.= w by RFINSEQ:8 ;
hence w in rng f by FUNCT_2:4, A17; :: thesis: verum

end;

then REAL (m + n) c= rng f ;
hence f is onto by XBOOLE_0:def 10; :: thesis: verum