for n being Nat
for m being Nat of n
for RAS being ReperAlgebra of n st RAS has_property_of_zero_in m & RAS is_additive_in m holds
RAS is_semi_additive_in m