theorem Th13: :: NUMBER08:13

for b being finite-support Function holds dom (b * (canFS (support b))) = dom (canFS (support b))