for X being real-membered set
for a being Real st a <> 0 holds
card X = card (a ** X) by Th3, CARD_1:5;