let M, N be non empty MetrSpace; :: thesis: [:(TopSpaceMetr M),(TopSpaceMetr N):] = TopSpaceMetr (max-Prod2 (M,N))

set S = TopSpaceMetr M;

set T = TopSpaceMetr N;

A1: TopSpaceMetr (max-Prod2 (M,N)) = TopStruct(# the carrier of (max-Prod2 (M,N)),(Family_open_set (max-Prod2 (M,N))) #) by PCOMPS_1:def 5;

A2: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def 5;

A3: TopSpaceMetr N = TopStruct(# the carrier of N,(Family_open_set N) #) by PCOMPS_1:def 5;

A4: the carrier of [:(TopSpaceMetr M),(TopSpaceMetr N):] = [: the carrier of (TopSpaceMetr M), the carrier of (TopSpaceMetr N):] by BORSUK_1:def 2

.= the carrier of (TopSpaceMetr (max-Prod2 (M,N))) by A1, A2, A3, Def1 ;

A5: the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] = { (union A) where A is Subset-Family of [:(TopSpaceMetr M),(TopSpaceMetr N):] : A c= { [:X1,X2:] where X1 is Subset of (TopSpaceMetr M), X2 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & X2 in the topology of (TopSpaceMetr N) ) } } by BORSUK_1:def 2;

the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] = the topology of (TopSpaceMetr (max-Prod2 (M,N)))

set S = TopSpaceMetr M;

set T = TopSpaceMetr N;

A1: TopSpaceMetr (max-Prod2 (M,N)) = TopStruct(# the carrier of (max-Prod2 (M,N)),(Family_open_set (max-Prod2 (M,N))) #) by PCOMPS_1:def 5;

A2: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def 5;

A3: TopSpaceMetr N = TopStruct(# the carrier of N,(Family_open_set N) #) by PCOMPS_1:def 5;

A4: the carrier of [:(TopSpaceMetr M),(TopSpaceMetr N):] = [: the carrier of (TopSpaceMetr M), the carrier of (TopSpaceMetr N):] by BORSUK_1:def 2

.= the carrier of (TopSpaceMetr (max-Prod2 (M,N))) by A1, A2, A3, Def1 ;

A5: the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] = { (union A) where A is Subset-Family of [:(TopSpaceMetr M),(TopSpaceMetr N):] : A c= { [:X1,X2:] where X1 is Subset of (TopSpaceMetr M), X2 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & X2 in the topology of (TopSpaceMetr N) ) } } by BORSUK_1:def 2;

the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] = the topology of (TopSpaceMetr (max-Prod2 (M,N)))

proof

hence
[:(TopSpaceMetr M),(TopSpaceMetr N):] = TopSpaceMetr (max-Prod2 (M,N))
by A4; :: thesis: verum
thus
the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] c= the topology of (TopSpaceMetr (max-Prod2 (M,N)))
:: according to XBOOLE_0:def 10 :: thesis: the topology of (TopSpaceMetr (max-Prod2 (M,N))) c= the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):]

assume A27: X in the topology of (TopSpaceMetr (max-Prod2 (M,N))) ; :: thesis: X in the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):]

then reconsider Y = X as Subset of [:(TopSpaceMetr M),(TopSpaceMetr N):] by A4;

A28: Base-Appr Y = { [:X1,Y1:] where X1 is Subset of (TopSpaceMetr M), Y1 is Subset of (TopSpaceMetr N) : ( [:X1,Y1:] c= Y & X1 is open & Y1 is open ) } by BORSUK_1:def 3;

A29: union (Base-Appr Y) = Y

end;proof

let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in the topology of (TopSpaceMetr (max-Prod2 (M,N))) or X in the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] )
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] or X in the topology of (TopSpaceMetr (max-Prod2 (M,N))) )

assume A6: X in the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] ; :: thesis: X in the topology of (TopSpaceMetr (max-Prod2 (M,N)))

then consider A being Subset-Family of [:(TopSpaceMetr M),(TopSpaceMetr N):] such that

A7: X = union A and

A8: A c= { [:X1,X2:] where X1 is Subset of (TopSpaceMetr M), X2 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & X2 in the topology of (TopSpaceMetr N) ) } by A5;

for x being Point of (max-Prod2 (M,N)) st x in union A holds

ex r being Real st

( r > 0 & Ball (x,r) c= union A )

end;assume A6: X in the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] ; :: thesis: X in the topology of (TopSpaceMetr (max-Prod2 (M,N)))

then consider A being Subset-Family of [:(TopSpaceMetr M),(TopSpaceMetr N):] such that

A7: X = union A and

A8: A c= { [:X1,X2:] where X1 is Subset of (TopSpaceMetr M), X2 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & X2 in the topology of (TopSpaceMetr N) ) } by A5;

for x being Point of (max-Prod2 (M,N)) st x in union A holds

ex r being Real st

( r > 0 & Ball (x,r) c= union A )

proof

hence
X in the topology of (TopSpaceMetr (max-Prod2 (M,N)))
by A1, A4, A6, PCOMPS_1:def 4, A7; :: thesis: verum
let x be Point of (max-Prod2 (M,N)); :: thesis: ( x in union A implies ex r being Real st

( r > 0 & Ball (x,r) c= union A ) )

assume x in union A ; :: thesis: ex r being Real st

( r > 0 & Ball (x,r) c= union A )

then consider Z being set such that

A9: x in Z and

A10: Z in A by TARSKI:def 4;

Z in { [:X1,X2:] where X1 is Subset of (TopSpaceMetr M), X2 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & X2 in the topology of (TopSpaceMetr N) ) } by A8, A10;

then consider X1 being Subset of (TopSpaceMetr M), X2 being Subset of (TopSpaceMetr N) such that

A11: Z = [:X1,X2:] and

A12: X1 in the topology of (TopSpaceMetr M) and

A13: X2 in the topology of (TopSpaceMetr N) ;

consider z1, z2 being object such that

A14: z1 in X1 and

A15: z2 in X2 and

A16: x = [z1,z2] by A9, A11, ZFMISC_1:def 2;

reconsider z2 = z2 as Point of N by A3, A15;

consider r2 being Real such that

A17: r2 > 0 and

A18: Ball (z2,r2) c= X2 by A3, A13, A15, PCOMPS_1:def 4;

reconsider z1 = z1 as Point of M by A2, A14;

consider r1 being Real such that

A19: r1 > 0 and

A20: Ball (z1,r1) c= X1 by A2, A12, A14, PCOMPS_1:def 4;

take r = min (r1,r2); :: thesis: ( r > 0 & Ball (x,r) c= union A )

thus r > 0 by A19, A17, XXREAL_0:15; :: thesis: Ball (x,r) c= union A

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in Ball (x,r) or b in union A )

assume A21: b in Ball (x,r) ; :: thesis: b in union A

then reconsider bb = b as Point of (max-Prod2 (M,N)) ;

A22: dist (bb,x) < r by A21, METRIC_1:11;

consider x1, y1 being Point of M, x2, y2 being Point of N such that

A23: bb = [x1,x2] and

A24: x = [y1,y2] and

A25: the distance of (max-Prod2 (M,N)) . (bb,x) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by Def1;

z2 = y2 by A16, A24, XTUPLE_0:1;

then the distance of N . (x2,z2) <= max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by XXREAL_0:25;

then ( min (r1,r2) <= r2 & the distance of N . (x2,z2) < r ) by A25, A22, XXREAL_0:2, XXREAL_0:17;

then dist (x2,z2) < r2 by XXREAL_0:2;

then A26: x2 in Ball (z2,r2) by METRIC_1:11;

z1 = y1 by A16, A24, XTUPLE_0:1;

then the distance of M . (x1,z1) <= max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by XXREAL_0:25;

then ( min (r1,r2) <= r1 & the distance of M . (x1,z1) < r ) by A25, A22, XXREAL_0:2, XXREAL_0:17;

then dist (x1,z1) < r1 by XXREAL_0:2;

then x1 in Ball (z1,r1) by METRIC_1:11;

then b in [:X1,X2:] by A20, A18, A23, A26, ZFMISC_1:87;

hence b in union A by A10, A11, TARSKI:def 4; :: thesis: verum

end;( r > 0 & Ball (x,r) c= union A ) )

assume x in union A ; :: thesis: ex r being Real st

( r > 0 & Ball (x,r) c= union A )

then consider Z being set such that

A9: x in Z and

A10: Z in A by TARSKI:def 4;

Z in { [:X1,X2:] where X1 is Subset of (TopSpaceMetr M), X2 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & X2 in the topology of (TopSpaceMetr N) ) } by A8, A10;

then consider X1 being Subset of (TopSpaceMetr M), X2 being Subset of (TopSpaceMetr N) such that

A11: Z = [:X1,X2:] and

A12: X1 in the topology of (TopSpaceMetr M) and

A13: X2 in the topology of (TopSpaceMetr N) ;

consider z1, z2 being object such that

A14: z1 in X1 and

A15: z2 in X2 and

A16: x = [z1,z2] by A9, A11, ZFMISC_1:def 2;

reconsider z2 = z2 as Point of N by A3, A15;

consider r2 being Real such that

A17: r2 > 0 and

A18: Ball (z2,r2) c= X2 by A3, A13, A15, PCOMPS_1:def 4;

reconsider z1 = z1 as Point of M by A2, A14;

consider r1 being Real such that

A19: r1 > 0 and

A20: Ball (z1,r1) c= X1 by A2, A12, A14, PCOMPS_1:def 4;

take r = min (r1,r2); :: thesis: ( r > 0 & Ball (x,r) c= union A )

thus r > 0 by A19, A17, XXREAL_0:15; :: thesis: Ball (x,r) c= union A

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in Ball (x,r) or b in union A )

assume A21: b in Ball (x,r) ; :: thesis: b in union A

then reconsider bb = b as Point of (max-Prod2 (M,N)) ;

A22: dist (bb,x) < r by A21, METRIC_1:11;

consider x1, y1 being Point of M, x2, y2 being Point of N such that

A23: bb = [x1,x2] and

A24: x = [y1,y2] and

A25: the distance of (max-Prod2 (M,N)) . (bb,x) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by Def1;

z2 = y2 by A16, A24, XTUPLE_0:1;

then the distance of N . (x2,z2) <= max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by XXREAL_0:25;

then ( min (r1,r2) <= r2 & the distance of N . (x2,z2) < r ) by A25, A22, XXREAL_0:2, XXREAL_0:17;

then dist (x2,z2) < r2 by XXREAL_0:2;

then A26: x2 in Ball (z2,r2) by METRIC_1:11;

z1 = y1 by A16, A24, XTUPLE_0:1;

then the distance of M . (x1,z1) <= max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by XXREAL_0:25;

then ( min (r1,r2) <= r1 & the distance of M . (x1,z1) < r ) by A25, A22, XXREAL_0:2, XXREAL_0:17;

then dist (x1,z1) < r1 by XXREAL_0:2;

then x1 in Ball (z1,r1) by METRIC_1:11;

then b in [:X1,X2:] by A20, A18, A23, A26, ZFMISC_1:87;

hence b in union A by A10, A11, TARSKI:def 4; :: thesis: verum

assume A27: X in the topology of (TopSpaceMetr (max-Prod2 (M,N))) ; :: thesis: X in the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):]

then reconsider Y = X as Subset of [:(TopSpaceMetr M),(TopSpaceMetr N):] by A4;

A28: Base-Appr Y = { [:X1,Y1:] where X1 is Subset of (TopSpaceMetr M), Y1 is Subset of (TopSpaceMetr N) : ( [:X1,Y1:] c= Y & X1 is open & Y1 is open ) } by BORSUK_1:def 3;

A29: union (Base-Appr Y) = Y

proof

Base-Appr Y c= { [:X1,Y1:] where X1 is Subset of (TopSpaceMetr M), Y1 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & Y1 in the topology of (TopSpaceMetr N) ) }
thus
union (Base-Appr Y) c= Y
by BORSUK_1:12; :: according to XBOOLE_0:def 10 :: thesis: Y c= union (Base-Appr Y)

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in Y or u in union (Base-Appr Y) )

assume A30: u in Y ; :: thesis: u in union (Base-Appr Y)

then reconsider uu = u as Point of (max-Prod2 (M,N)) by A1, A4;

consider r being Real such that

A31: r > 0 and

A32: Ball (uu,r) c= Y by A1, A27, A30, PCOMPS_1:def 4;

uu in the carrier of (max-Prod2 (M,N)) ;

then uu in [: the carrier of M, the carrier of N:] by Def1;

then consider u1, u2 being object such that

A33: u1 in the carrier of M and

A34: u2 in the carrier of N and

A35: u = [u1,u2] by ZFMISC_1:def 2;

reconsider u2 = u2 as Point of N by A34;

reconsider u1 = u1 as Point of M by A33;

reconsider B2 = Ball (u2,r) as Subset of (TopSpaceMetr N) by A3;

reconsider B1 = Ball (u1,r) as Subset of (TopSpaceMetr M) by A2;

( u1 in Ball (u1,r) & u2 in Ball (u2,r) ) by A31, TBSP_1:11;

then A36: u in [:B1,B2:] by A35, ZFMISC_1:87;

A37: [:B1,B2:] c= Y

then [:B1,B2:] in Base-Appr Y by A28, A37;

hence u in union (Base-Appr Y) by A36, TARSKI:def 4; :: thesis: verum

end;let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in Y or u in union (Base-Appr Y) )

assume A30: u in Y ; :: thesis: u in union (Base-Appr Y)

then reconsider uu = u as Point of (max-Prod2 (M,N)) by A1, A4;

consider r being Real such that

A31: r > 0 and

A32: Ball (uu,r) c= Y by A1, A27, A30, PCOMPS_1:def 4;

uu in the carrier of (max-Prod2 (M,N)) ;

then uu in [: the carrier of M, the carrier of N:] by Def1;

then consider u1, u2 being object such that

A33: u1 in the carrier of M and

A34: u2 in the carrier of N and

A35: u = [u1,u2] by ZFMISC_1:def 2;

reconsider u2 = u2 as Point of N by A34;

reconsider u1 = u1 as Point of M by A33;

reconsider B2 = Ball (u2,r) as Subset of (TopSpaceMetr N) by A3;

reconsider B1 = Ball (u1,r) as Subset of (TopSpaceMetr M) by A2;

( u1 in Ball (u1,r) & u2 in Ball (u2,r) ) by A31, TBSP_1:11;

then A36: u in [:B1,B2:] by A35, ZFMISC_1:87;

A37: [:B1,B2:] c= Y

proof

( B1 is open & B2 is open )
by TOPMETR:14;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [:B1,B2:] or x in Y )

assume x in [:B1,B2:] ; :: thesis: x in Y

then consider x1, x2 being object such that

A38: x1 in B1 and

A39: x2 in B2 and

A40: x = [x1,x2] by ZFMISC_1:def 2;

reconsider x2 = x2 as Point of N by A39;

reconsider x1 = x1 as Point of M by A38;

consider p1, p2 being Point of M, q1, q2 being Point of N such that

A41: ( uu = [p1,q1] & [x1,x2] = [p2,q2] ) and

A42: the distance of (max-Prod2 (M,N)) . (uu,[x1,x2]) = max (( the distance of M . (p1,p2)),( the distance of N . (q1,q2))) by Def1;

( u2 = q1 & x2 = q2 ) by A35, A41, XTUPLE_0:1;

then A43: dist (q1,q2) < r by A39, METRIC_1:11;

( u1 = p1 & x1 = p2 ) by A35, A41, XTUPLE_0:1;

then dist (p1,p2) < r by A38, METRIC_1:11;

then dist (uu,[x1,x2]) < r by A42, A43, XXREAL_0:16;

then x in Ball (uu,r) by A40, METRIC_1:11;

hence x in Y by A32; :: thesis: verum

end;assume x in [:B1,B2:] ; :: thesis: x in Y

then consider x1, x2 being object such that

A38: x1 in B1 and

A39: x2 in B2 and

A40: x = [x1,x2] by ZFMISC_1:def 2;

reconsider x2 = x2 as Point of N by A39;

reconsider x1 = x1 as Point of M by A38;

consider p1, p2 being Point of M, q1, q2 being Point of N such that

A41: ( uu = [p1,q1] & [x1,x2] = [p2,q2] ) and

A42: the distance of (max-Prod2 (M,N)) . (uu,[x1,x2]) = max (( the distance of M . (p1,p2)),( the distance of N . (q1,q2))) by Def1;

( u2 = q1 & x2 = q2 ) by A35, A41, XTUPLE_0:1;

then A43: dist (q1,q2) < r by A39, METRIC_1:11;

( u1 = p1 & x1 = p2 ) by A35, A41, XTUPLE_0:1;

then dist (p1,p2) < r by A38, METRIC_1:11;

then dist (uu,[x1,x2]) < r by A42, A43, XXREAL_0:16;

then x in Ball (uu,r) by A40, METRIC_1:11;

hence x in Y by A32; :: thesis: verum

then [:B1,B2:] in Base-Appr Y by A28, A37;

hence u in union (Base-Appr Y) by A36, TARSKI:def 4; :: thesis: verum

proof

hence
X in the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):]
by A5, A29; :: thesis: verum
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in Base-Appr Y or A in { [:X1,Y1:] where X1 is Subset of (TopSpaceMetr M), Y1 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & Y1 in the topology of (TopSpaceMetr N) ) } )

assume A in Base-Appr Y ; :: thesis: A in { [:X1,Y1:] where X1 is Subset of (TopSpaceMetr M), Y1 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & Y1 in the topology of (TopSpaceMetr N) ) }

then consider X1 being Subset of (TopSpaceMetr M), Y1 being Subset of (TopSpaceMetr N) such that

A44: A = [:X1,Y1:] and

[:X1,Y1:] c= Y and

A45: ( X1 is open & Y1 is open ) by A28;

( X1 in the topology of (TopSpaceMetr M) & Y1 in the topology of (TopSpaceMetr N) ) by A45;

hence A in { [:X1,Y1:] where X1 is Subset of (TopSpaceMetr M), Y1 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & Y1 in the topology of (TopSpaceMetr N) ) } by A44; :: thesis: verum

end;assume A in Base-Appr Y ; :: thesis: A in { [:X1,Y1:] where X1 is Subset of (TopSpaceMetr M), Y1 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & Y1 in the topology of (TopSpaceMetr N) ) }

then consider X1 being Subset of (TopSpaceMetr M), Y1 being Subset of (TopSpaceMetr N) such that

A44: A = [:X1,Y1:] and

[:X1,Y1:] c= Y and

A45: ( X1 is open & Y1 is open ) by A28;

( X1 in the topology of (TopSpaceMetr M) & Y1 in the topology of (TopSpaceMetr N) ) by A45;

hence A in { [:X1,Y1:] where X1 is Subset of (TopSpaceMetr M), Y1 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & Y1 in the topology of (TopSpaceMetr N) ) } by A44; :: thesis: verum