for T1, T2 being TopSpace holds weight [:T1,T2:] c= (weight T1) *` (weight T2)