let A, B be Subset of REAL; 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
object ;
TARSKI:def 3 ( 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:63;
A2:
((1,2) --> (A,B)) . 2
= B
by FUNCT_4:63;
assume
a in product ((1,2) --> (A,B))
;
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
object 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:62;
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;
dom <*(g . 1),(g . 2)*> = {1,2}
by FINSEQ_1:2, FINSEQ_1:89;
then
a = |[m,n]|
by A3, A4, A8, FUNCT_1:2, FUNCT_4:62;
hence
a in the
carrier of
(TOP-REAL 2)
;
verum
end;
hence
product ((1,2) --> (A,B)) is Subset of (TOP-REAL 2)
; verum