let X be real-membered set ; :: thesis: for a being real number st a <> 0 holds
card X = card (a ** X)
let a be real number ; :: thesis: ( a <> 0 implies card X = card (a ** X) )
assume a <> 0 ; :: thesis: card X = card (a ** X)
then X,a ** X are_equipotent by Th3;
hence card X = card (a ** X) by CARD_1:21; :: thesis: verum