let n be Element of 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 7 :: 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 A3: p . m = pm ; :: thesis: *' a,(p +* m,(a @ pm)) = a @ (*' a,p)
*' a,(p +* m,(a @ pm)) = (*' a,p) @ (*' a,(p +* m,a)) by A2, A3, Def8
.= a @ (*' a,p) by A1, Def6 ;
hence *' a,(p +* m,(a @ pm)) = a @ (*' a,p) ; :: thesis: verum