theorem Th1: :: EUCLID_4:1

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