let n be 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
let m be 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
let RAS be ReperAlgebra of n; ( RAS has_property_of_zero_in m & RAS is_additive_in m implies RAS is_semi_additive_in m )
assume that
A1:
RAS has_property_of_zero_in m
and
A2:
RAS is_additive_in m
; RAS is_semi_additive_in m
let a be Point of RAS; MIDSP_3:def 5 for pii being Point of RAS
for p being Tuple of (n + 1),RAS st p . m = pii holds
*' (a,(p +* (m,(a @ pii)))) = a @ (*' (a,p))
let pm be Point of RAS; for p being Tuple of (n + 1),RAS st p . m = pm holds
*' (a,(p +* (m,(a @ pm)))) = a @ (*' (a,p))
let p be Tuple of (n + 1),RAS; ( p . m = pm implies *' (a,(p +* (m,(a @ pm)))) = a @ (*' (a,p)) )
assume
p . m = pm
; *' (a,(p +* (m,(a @ pm)))) = a @ (*' (a,p))
then *' (a,(p +* (m,(a @ pm)))) =
(*' (a,p)) @ (*' (a,(p +* (m,a))))
by A2
.=
a @ (*' (a,p))
by A1
;
hence
*' (a,(p +* (m,(a @ pm)))) = a @ (*' (a,p))
; verum