let n be Nat; :: thesis: for m being Nat of n
for RAS being ReperAlgebra of n
for W being ATLAS of RAS st RAS has_property_of_zero_in m holds
( RAS is_additive_in m iff for x being Tuple of (n + 1),W
for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) )
let m be Nat of n; :: thesis: for RAS being ReperAlgebra of n
for W being ATLAS of RAS st RAS has_property_of_zero_in m holds
( RAS is_additive_in m iff for x being Tuple of (n + 1),W
for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) )
let RAS be ReperAlgebra of n; :: thesis: for W being ATLAS of RAS st RAS has_property_of_zero_in m holds
( RAS is_additive_in m iff for x being Tuple of (n + 1),W
for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) )
let W be ATLAS of RAS; :: thesis: ( RAS has_property_of_zero_in m implies ( RAS is_additive_in m iff for x being Tuple of (n + 1),W
for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) ) )
assume A1: RAS has_property_of_zero_in m ; :: thesis: ( RAS is_additive_in m iff for x being Tuple of (n + 1),W
for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) )
thus ( RAS is_additive_in m implies for x being Tuple of (n + 1),W
for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) ) :: thesis: ( ( for x being Tuple of (n + 1),W
for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) ) implies RAS is_additive_in m )

proof

set a = the Point of RAS;
assume A2: RAS is_additive_in m ; :: thesis: for x being Tuple of (n + 1),W
for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v)))
let x be Tuple of (n + 1),W; :: thesis: for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v)))
let v be Vector of W; :: thesis: Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v)))
set p = ( the Point of RAS,x) . W;
set p9m = ( the Point of RAS,v) . W;
consider p99m being Point of RAS such that
A3: p99m @ the Point of RAS = ((( the Point of RAS,x) . W) . m) @ (( the Point of RAS,v) . W) by MIDSP_1:def 3;
A4: ( W . ( the Point of RAS,(( the Point of RAS,x) . W)) = x & W . ( the Point of RAS,(( the Point of RAS,v) . W)) = v ) by Th15, MIDSP_2:33;
A5: W . ( the Point of RAS,p99m) = (W . ( the Point of RAS,((( the Point of RAS,x) . W) . m))) + (W . ( the Point of RAS,(( the Point of RAS,v) . W))) by A3, MIDSP_2:30
.= (x . m) + v by A4, Def9 ;
(( the Point of RAS,x) . W) +* (m,p99m) = ( the Point of RAS,(x +* (m,((x . m) + v)))) . W

proof

set pp = (( the Point of RAS,x) . W) +* (m,p99m);
set xx = x +* (m,((x . m) + v));
set qq = ( the Point of RAS,(x +* (m,((x . m) + v)))) . W;
for i being Nat of n holds ((( the Point of RAS,x) . W) +* (m,p99m)) . i = (( the Point of RAS,(x +* (m,((x . m) + v)))) . W) . i

proof

let i be Nat of n; :: thesis: ((( the Point of RAS,x) . W) +* (m,p99m)) . i = (( the Point of RAS,(x +* (m,((x . m) + v)))) . W) . i

per cases ( i = m or i <> m ) ;

suppose A6: i = m ; :: thesis: ((( the Point of RAS,x) . W) +* (m,p99m)) . i = (( the Point of RAS,(x +* (m,((x . m) + v)))) . W) . i

hence ((( the Point of RAS,x) . W) +* (m,p99m)) . i = p99m by Th10
.= ( the Point of RAS,((x . m) + v)) . W by A5, MIDSP_2:33
.= ( the Point of RAS,((x +* (m,((x . m) + v))) . m)) . W by Th13
.= (( the Point of RAS,(x +* (m,((x . m) + v)))) . W) . i by A6, Def8 ;
:: thesis: verum

end;

suppose A7: i <> m ; :: thesis: ((( the Point of RAS,x) . W) +* (m,p99m)) . i = (( the Point of RAS,(x +* (m,((x . m) + v)))) . W) . i

hence ((( the Point of RAS,x) . W) +* (m,p99m)) . i = (( the Point of RAS,x) . W) . i by FUNCT_7:32
.= ( the Point of RAS,(x . i)) . W by Def8
.= ( the Point of RAS,((x +* (m,((x . m) + v))) . i)) . W by A7, FUNCT_7:32
.= (( the Point of RAS,(x +* (m,((x . m) + v)))) . W) . i by Def8 ;
:: thesis: verum

end;

end;

end;

hence (( the Point of RAS,x) . W) +* (m,p99m) = ( the Point of RAS,(x +* (m,((x . m) + v)))) . W by Th9; :: thesis: verum

end;

then A8: Phi (x +* (m,((x . m) + v))) = W . ( the Point of RAS,(*' ( the Point of RAS,((( the Point of RAS,x) . W) +* (m,p99m))))) by Lm5;
A9: (( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W)) = ( the Point of RAS,(x +* (m,v))) . W

proof

set pp = (( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W));
set qq = ( the Point of RAS,(x +* (m,v))) . W;
for i being Nat of n holds ((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))) . i = (( the Point of RAS,(x +* (m,v))) . W) . i

proof

let i be Nat of n; :: thesis: ((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))) . i = (( the Point of RAS,(x +* (m,v))) . W) . i

per cases ( i = m or i <> m ) ;

suppose A10: i = m ; :: thesis: ((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))) . i = (( the Point of RAS,(x +* (m,v))) . W) . i

hence ((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))) . i = ( the Point of RAS,v) . W by Th10
.= ( the Point of RAS,((x +* (m,v)) . m)) . W by Th13
.= (( the Point of RAS,(x +* (m,v))) . W) . i by A10, Def8 ;
:: thesis: verum

end;

suppose A11: i <> m ; :: thesis: ((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))) . i = (( the Point of RAS,(x +* (m,v))) . W) . i

hence ((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))) . i = (( the Point of RAS,x) . W) . i by FUNCT_7:32
.= ( the Point of RAS,(x . i)) . W by Def8
.= ( the Point of RAS,((x +* (m,v)) . i)) . W by A11, FUNCT_7:32
.= (( the Point of RAS,(x +* (m,v))) . W) . i by Def8 ;
:: thesis: verum

end;

end;

end;

hence (( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W)) = ( the Point of RAS,(x +* (m,v))) . W by Th9; :: thesis: verum

end;

( RAS is_semi_additive_in m & *' ( the Point of RAS,((( the Point of RAS,x) . W) +* (m,(((( the Point of RAS,x) . W) . m) @ (( the Point of RAS,v) . W))))) = (*' ( the Point of RAS,(( the Point of RAS,x) . W))) @ (*' ( the Point of RAS,((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))))) ) by A1, A2, Th29;
then A12: W . ( the Point of RAS,(*' ( the Point of RAS,((( the Point of RAS,x) . W) +* (m,p99m))))) = (W . ( the Point of RAS,(*' ( the Point of RAS,(( the Point of RAS,x) . W))))) + (W . ( the Point of RAS,(*' ( the Point of RAS,((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))))))) by A3, Lm6;
Phi x = W . ( the Point of RAS,(*' ( the Point of RAS,(( the Point of RAS,x) . W)))) by Lm5;
hence Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) by A12, A8, A9, Lm5; :: thesis: verum

end;

thus ( ( for x being Tuple of (n + 1),W
for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) ) implies RAS is_additive_in m ) :: thesis: verum

proof

assume A13: for x being Tuple of (n + 1),W
for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) ; :: thesis: RAS is_additive_in m
then A14: RAS is_semi_additive_in m by Lm7;
for a, pm, p9m being Point of RAS
for p being Tuple of (n + 1),RAS st p . m = pm holds
*' (a,(p +* (m,(pm @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m))))

proof

let a, pm, p9m be Point of RAS; :: thesis: for p being Tuple of (n + 1),RAS st p . m = pm holds
*' (a,(p +* (m,(pm @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m))))
let p be Tuple of (n + 1),RAS; :: thesis: ( p . m = pm implies *' (a,(p +* (m,(pm @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m)))) )
assume A15: p . m = pm ; :: thesis: *' (a,(p +* (m,(pm @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m))))
set x = W . (a,p);
set v = W . (a,p9m);
consider p99m being Point of RAS such that
A16: p99m @ a = (p . m) @ p9m by MIDSP_1:def 3;
A17: (a,(W . (a,p))) . W = p by Th15;
A18: W . (a,p99m) = (W . (a,(p . m))) + (W . (a,p9m)) by A16, MIDSP_2:30
.= ((W . (a,p)) . m) + (W . (a,p9m)) by Def9 ;
p +* (m,p99m) = (a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W

proof

set pp = p +* (m,p99m);
set xx = (W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m))));
set qq = (a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W;
for i being Nat of n holds (p +* (m,p99m)) . i = ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i

proof

let i be Nat of n; :: thesis: (p +* (m,p99m)) . i = ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i

per cases ( i = m or i <> m ) ;

suppose A19: i = m ; :: thesis: (p +* (m,p99m)) . i = ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i

hence (p +* (m,p99m)) . i = p99m by Th10
.= (a,(((W . (a,p)) . m) + (W . (a,p9m)))) . W by A18, MIDSP_2:33
.= (a,(((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m))))) . m)) . W by Th13
.= ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i by A19, Def8 ;
:: thesis: verum

end;

suppose A20: i <> m ; :: thesis: (p +* (m,p99m)) . i = ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i

hence (p +* (m,p99m)) . i = p . i by FUNCT_7:32
.= (a,((W . (a,p)) . i)) . W by A17, Def8
.= (a,(((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m))))) . i)) . W by A20, FUNCT_7:32
.= ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i by Def8 ;
:: thesis: verum

end;

end;

end;

hence p +* (m,p99m) = (a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W by Th9; :: thesis: verum

end;

then A21: Phi ((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m))))) = W . (a,(*' (a,(p +* (m,p99m))))) by Lm5;
A22: (a,(W . (a,p9m))) . W = p9m by MIDSP_2:33;
p +* (m,p9m) = (a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W

proof

set pp = p +* (m,p9m);
set qq = (a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W;
for i being Nat of n holds (p +* (m,p9m)) . i = ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i

proof

let i be Nat of n; :: thesis: (p +* (m,p9m)) . i = ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i

per cases ( i = m or i <> m ) ;

suppose A23: i = m ; :: thesis: (p +* (m,p9m)) . i = ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i

hence (p +* (m,p9m)) . i = p9m by Th10
.= (a,(((W . (a,p)) +* (m,(W . (a,p9m)))) . m)) . W by A22, Th13
.= ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i by A23, Def8 ;
:: thesis: verum

end;

suppose A24: i <> m ; :: thesis: (p +* (m,p9m)) . i = ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i

hence (p +* (m,p9m)) . i = p . i by FUNCT_7:32
.= (a,((W . (a,p)) . i)) . W by A17, Def8
.= (a,(((W . (a,p)) +* (m,(W . (a,p9m)))) . i)) . W by A24, FUNCT_7:32
.= ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i by Def8 ;
:: thesis: verum

end;

end;

end;

hence p +* (m,p9m) = (a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W by Th9; :: thesis: verum

end;

then A25: Phi ((W . (a,p)) +* (m,(W . (a,p9m)))) = W . (a,(*' (a,(p +* (m,p9m))))) by Lm5;
Phi (W . (a,p)) = W . (a,(*' (a,p))) by Lm4;
then W . (a,(*' (a,(p +* (m,p99m))))) = (W . (a,(*' (a,p)))) + (W . (a,(*' (a,(p +* (m,p9m)))))) by A13, A21, A25;
hence *' (a,(p +* (m,(pm @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m)))) by A14, A15, A16, Lm6; :: thesis: verum

end;

hence RAS is_additive_in m ; :: thesis: verum

end;