:: deftheorem defines 0* EUCLID:def 4 :
for n being Nat holds 0* n = n |-> (In (0,REAL));