for X being real-membered set
for a being Real st a <> 0 holds
X,a ** X are_equipotent