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) )
assume a in product (1,2 --> A,B) ; :: thesis: a in the carrier of (TOP-REAL 2)
then consider g being Function such that
A1: a = g and
A2: dom g = dom (1,2 --> A,B) and
A3: 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;
A4: dom (1,2 --> A,B) = {1,2} by FUNCT_4:65;
then A5: ( 1 in dom (1,2 --> A,B) & 2 in dom (1,2 --> A,B) ) by TARSKI:def 2;
( (1,2 --> A,B) . 1 = A & (1,2 --> A,B) . 2 = B ) by FUNCT_4:66;
then ( g . 1 in A & g . 2 in B ) by A3, A5;
then reconsider m = g . 1, n = g . 2 as Real ;
A6: 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 A2, TARSKI:def 2;
hence g . k = <*(g . 1),(g . 2)*> . k by FINSEQ_1:61; :: thesis: verum

end;

then a = |[m,n]| by A1, A2, A4, A6, FUNCT_1:9;
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