theorem Th3: :: EUCLID_4:3

for n being Nat
for x being Element of REAL n holds
( 1 * x = x & 0 * x = 0* n )