let A, B be Subset of REAL ; :: thesis: product (1,2 --> A,B) is Subset of (TOP-REAL 2)
set f = 1,2 --> A,B;
product (1,2 --> A,B) c= the carrier of (TOP-REAL 2)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in product (1,2 --> A,B) or a in the carrier of (TOP-REAL 2) )
A1: (1,2 --> A,B) . 1 = A by FUNCT_4:66;
A2: (1,2 --> A,B) . 2 = B by FUNCT_4:66;
assume a in product (1,2 --> A,B) ; :: thesis: a in the carrier of (TOP-REAL 2)
then consider g being Function such that
A3: a = g and
A4: dom g = dom (1,2 --> A,B) and
A5: 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;
A6: dom (1,2 --> A,B) = {1,2} by FUNCT_4:65;
then 2 in dom (1,2 --> A,B) by TARSKI:def 2;
then A7: g . 2 in B by A5, A2;
1 in dom (1,2 --> A,B) by A6, TARSKI:def 2;
then g . 1 in A by A5, A1;
then reconsider m = g . 1, n = g . 2 as Real by A7;

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

end;

dom <*(g . 1),(g . 2)*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
then a = |[m,n]| by A3, A4, A8, FUNCT_1:9, FUNCT_4:65;
hence a in the carrier of (TOP-REAL 2) ; :: thesis: verum

end;

hence product (1,2 --> A,B) is Subset of (TOP-REAL 2) ; :: thesis: verum