let T1, T2 be TopSpace; :: thesis: weight [:T1,T2:] c= (weight T1) *` (weight T2)

per cases ( T1 is empty or T2 is empty or ( not T1 is empty & not T2 is empty ) ) ;

suppose ( T1 is empty or T2 is empty ) ; :: thesis: weight [:T1,T2:] c= (weight T1) *` (weight T2)

hence weight [:T1,T2:] c= (weight T1) *` (weight T2) ; :: thesis: verum

end;

suppose A1: ( not T1 is empty & not T2 is empty ) ; :: thesis: weight [:T1,T2:] c= (weight T1) *` (weight T2)

consider B2 being Basis of T2 such that
A2: card B2 = weight T2 by WAYBEL23:74;
consider B1 being Basis of T1 such that
A3: card B1 = weight T1 by WAYBEL23:74;
reconsider B12 = { [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 ) } as Basis of [:T1,T2:] by A1, YELLOW_9:40;
reconsider B1 = B1, B2 = B2, B12 = B12 as non empty set by A1, YELLOW12:34;
deffunc H₁( Element of [:B1,B2:]) -> set = [:($1 `1),($1 `2):];
A4: for x being Element of [:B1,B2:] holds H₁(x) is Element of B12

proof

let x be Element of [:B1,B2:]; :: thesis: H₁(x) is Element of B12
( x `1 in B1 & x `2 in B2 ) ;
then H₁(x) in B12 ;
hence H₁(x) is Element of B12 ; :: thesis: verum

end;

consider f being Function of [:B1,B2:],B12 such that
A5: for x being Element of [:B1,B2:] holds f . x = H₁(x) from FUNCT_2:sch 9(A4);
A6: dom f = [:B1,B2:] by FUNCT_2:def 1;
B12 c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B12 or x in rng f )
assume x in B12 ; :: thesis: x in rng f
then consider a being Subset of T1, b being Subset of T2 such that
A7: x = [:a,b:] and
A8: ( a in B1 & b in B2 ) ;
reconsider ab = [a,b] as Element of [:B1,B2:] by A8, ZFMISC_1:87;
( [a,b] `1 = a & [a,b] `2 = b ) ;
then x = f . ab by A5, A7;
hence x in rng f by A6, FUNCT_1:def 3; :: thesis: verum

end;

then A9: ( weight [:T1,T2:] c= card B12 & card B12 c= card [:B1,B2:] ) by A6, CARD_1:12, WAYBEL23:73;
card [:B1,B2:] = card [:(card B1),(card B2):] by CARD_2:7
.= (card B1) *` (card B2) by CARD_2:def 2 ;
hence weight [:T1,T2:] c= (weight T1) *` (weight T2) by A3, A2, A9; :: thesis: verum

end;

end;