let T1, T2 be TopSpace; 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 A1:
( not
T1 is
empty & not
T2 is
empty )
;
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 H1(
Element of
[:B1,B2:])
-> set =
[:($1 `1),($1 `2):];
A4:
for
x being
Element of
[:B1,B2:] holds
H1(
x) is
Element of
B12
consider f being
Function of
[:B1,B2:],
B12 such that A5:
for
x being
Element of
[:B1,B2:] holds
f . x = H1(
x)
from FUNCT_2:sch 9(A4);
A6:
dom f = [:B1,B2:]
by FUNCT_2:def 1;
B12 c= rng f
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;
verum end; end;