:: deftheorem defines has_property_of_zero_in MIDSP_3:def 4 :
for n, i being Nat
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2 holds
( RAS has_property_of_zero_in i iff for a being Point of RAS
for p being Tuple of (n + 1),RAS holds *' (a,(p +* (i,a))) = a );