let n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: RAS is_semi_additive_in m
let a be Point of RAS; :: according to MIDSP_3:def 5 :: thesis: 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; :: thesis: 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; :: thesis: ( p . m = pm implies *' (a,(p +* (m,(a @ pm)))) = a @ (*' (a,p)) )
assume p . m = pm ; :: thesis: *' (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)) ; :: thesis: verum