theorem Th3: :: INT_4:3

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