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

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