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;
A3: ( (1,2 --> A,B) . 1 = A & (1,2 --> A,B) . 2 = B ) by FUNCT_4:66;
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
A4: a in the carrier of [:R^1 ,R^1 :] and
A5: a in [:A,B:] and
A6: f . a = x by FUNCT_2:115;
reconsider a = a as Point of [:R^1 ,R^1 :] by A4;
consider m, n being set such that
A7: ( m in A & n in B ) and
A8: a = [m,n] by A5, ZFMISC_1:def 2;
reconsider m = m, n = n as Real by A7;
f . a = x by A6;
then reconsider g = x as Function of Seg 2, REAL by EUCLID:26;
A9: dom g = dom (1,2 --> A,B) by A2, FINSEQ_1:4, FUNCT_2:def 1;
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 )
assume y in dom (1,2 --> A,B) ; :: thesis: g . y in (1,2 --> A,B) . y
then A10: ( y = 1 or y = 2 ) by TARSKI:def 2;
A11: f . [m,n] = |[m,n]| by A1;
( |[m,n]| `1 = m & |[m,n]| `2 = n ) by EUCLID:56;
hence g . y in (1,2 --> A,B) . y by A6, A7, A8, A10, A11, FUNCT_4:66; :: thesis: verum

end;

hence x in product (1,2 --> A,B) by A9, CARD_3:18; :: thesis: verum

end;

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
A12: a = g and
A13: dom g = dom (1,2 --> A,B) and
A14: 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;
( 1 in dom (1,2 --> A,B) & 2 in dom (1,2 --> A,B) ) by A2, TARSKI:def 2;
then A15: ( g . 1 in A & g . 2 in B ) by A3, A14;
then A16: [(g . 1),(g . 2)] in [:A,B:] by ZFMISC_1:106;
A17: dom <*(g . 1),(g . 2)*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;

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 A13, TARSKI:def 2;
hence g . k = <*(g . 1),(g . 2)*> . k by FINSEQ_1:61; :: thesis: verum

end;

then A18: a = <*(g . 1),(g . 2)*> by A2, A12, A13, A17, FUNCT_1:9;
the carrier of [:R^1 ,R^1 :] = [:the carrier of R^1 ,the carrier of R^1 :] by BORSUK_1:def 5;
then A19: [(g . 1),(g . 2)] in the carrier of [:R^1 ,R^1 :] by A15, TOPMETR:24, ZFMISC_1:106;
f . [(g . 1),(g . 2)] = <*(g . 1),(g . 2)*> by A1, A15;
hence a in f .: [:A,B:] by A16, A18, A19, FUNCT_2:43; :: thesis: verum