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