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