let A, B be Subset of REAL ; :: thesis: for f being Function of [:R^1 ,R^1 :],(TOP-REAL 2) st ( for x, y being Real holds f . [x,y] = <*x,y*> ) holds
f .: [:A,B:] = product (1,2 --> A,B)
let f be Function of [:R^1 ,R^1 :],(TOP-REAL 2); :: thesis: ( ( for x, y being Real holds f . [x,y] = <*x,y*> ) implies f .: [:A,B:] = product (1,2 --> A,B) )
assume A1: for x, y being Real holds f . [x,y] = <*x,y*> ; :: thesis: f .: [:A,B:] = product (1,2 --> A,B)
set h = 1,2 --> A,B;
A2: dom (1,2 --> A,B) = {1,2} by FUNCT_4:65;
thus f .: [:A,B:] c= product (1,2 --> A,B) :: according to XBOOLE_0:def 10 :: thesis: product (1,2 --> A,B) c= f .: [:A,B:]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in f .: [:A,B:] or x in product (1,2 --> A,B) )
assume x in f .: [:A,B:] ; :: thesis: x in product (1,2 --> A,B)
then consider a being set such that
A3: a in the carrier of [:R^1 ,R^1 :] and
A4: a in [:A,B:] and
A5: f . a = x by FUNCT_2:115;
reconsider a = a as Point of [:R^1 ,R^1 :] by A3;
consider m, n being set such that
A6: m in A and
A7: n in B and
A8: a = [m,n] by A4, ZFMISC_1:def 2;
f . a = x by A5;
then reconsider g = x as Function of (Seg 2),REAL by EUCLID:26;
reconsider m = m, n = n as Real by A6, A7;
A9: for y being set st y in dom (1,2 --> A,B) holds
g . y in (1,2 --> A,B) . y

proof

let y be set ; :: thesis: ( y in dom (1,2 --> A,B) implies g . y in (1,2 --> A,B) . y )
A10: |[m,n]| `1 = m by EUCLID:56;
assume y in dom (1,2 --> A,B) ; :: thesis: g . y in (1,2 --> A,B) . y
then A11: ( y = 1 or y = 2 ) by TARSKI:def 2;
A12: |[m,n]| `2 = n by EUCLID:56;
f . [m,n] = |[m,n]| by A1;
hence g . y in (1,2 --> A,B) . y by A5, A6, A7, A8, A11, A10, A12, FUNCT_4:66; :: thesis: verum

end;

dom g = dom (1,2 --> A,B) by A2, FINSEQ_1:4, FUNCT_2:def 1;
hence x in product (1,2 --> A,B) by A9, CARD_3:18; :: thesis: verum

end;

A13: (1,2 --> A,B) . 2 = B by FUNCT_4:66;
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in product (1,2 --> A,B) or a in f .: [:A,B:] )
assume a in product (1,2 --> A,B) ; :: thesis: a in f .: [:A,B:]
then consider g being Function such that
A14: a = g and
A15: dom g = dom (1,2 --> A,B) and
A16: for x being set st x in dom (1,2 --> A,B) holds
g . x in (1,2 --> A,B) . x by CARD_3:def 5;
2 in dom (1,2 --> A,B) by A2, TARSKI:def 2;
then A17: g . 2 in B by A13, A16;
A18: (1,2 --> A,B) . 1 = A by FUNCT_4:66;
1 in dom (1,2 --> A,B) by A2, TARSKI:def 2;
then A19: g . 1 in A by A18, A16;
then A20: f . [(g . 1),(g . 2)] = <*(g . 1),(g . 2)*> by A1, A17;

A21: now

let k be set ; :: thesis: ( k in dom g implies g . k = <*(g . 1),(g . 2)*> . k )
assume k in dom g ; :: thesis: g . k = <*(g . 1),(g . 2)*> . k
then ( k = 1 or k = 2 ) by A15, TARSKI:def 2;
hence g . k = <*(g . 1),(g . 2)*> . k by FINSEQ_1:61; :: thesis: verum

end;

A22: dom <*(g . 1),(g . 2)*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
A23: [(g . 1),(g . 2)] in [:A,B:] by A19, A17, ZFMISC_1:106;
the carrier of [:R^1 ,R^1 :] = [:the carrier of R^1 ,the carrier of R^1 :] by BORSUK_1:def 5;
then [(g . 1),(g . 2)] in the carrier of [:R^1 ,R^1 :] by A19, A17, TOPMETR:24, ZFMISC_1:106;
hence a in f .: [:A,B:] by A2, A14, A15, A23, A22, A21, A20, FUNCT_1:9, FUNCT_2:43; :: thesis: verum