let n be Element of 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

consider a being 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 = a,x . W;
set p9m = a,v . W;
consider p99m being Point of RAS such that
A3: p99m @ a = ((a,x . W) . m) @ (a,v . W) by MIDSP_1:def 4;
A4: ( W . a,(a,x . W) = x & W . a,(a,v . W) = v ) by Th17, MIDSP_2:39;
A5: W . a,p99m = (W . a,((a,x . W) . m)) + (W . a,(a,v . W)) by A3, MIDSP_2:36
.= (x . m) + v by A4, Def12 ;
(a,x . W) +* m,p99m = a,(x +* m,((x . m) + v)) . W

proof

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

proof

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

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

suppose A6: i = m ; :: thesis: ((a,x . W) +* m,p99m) . i = (a,(x +* m,((x . m) + v)) . W) . i

hence ((a,x . W) +* m,p99m) . i = p99m by Th12
.= a,((x . m) + v) . W by A5, MIDSP_2:39
.= a,((x +* m,((x . m) + v)) . m) . W by Th15
.= (a,(x +* m,((x . m) + v)) . W) . i by A6, Def11 ;
:: thesis: verum

end;

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

hence ((a,x . W) +* m,p99m) . i = (a,x . W) . i by FUNCT_7:34
.= a,(x . i) . W by Def11
.= a,((x +* m,((x . m) + v)) . i) . W by A7, FUNCT_7:34
.= (a,(x +* m,((x . m) + v)) . W) . i by Def11 ;
:: thesis: verum

end;

end;

end;

hence (a,x . W) +* m,p99m = a,(x +* m,((x . m) + v)) . W by Th11; :: thesis: verum

end;

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

proof

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

proof

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

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

suppose A10: i = m ; :: thesis: ((a,x . W) +* m,(a,v . W)) . i = (a,(x +* m,v) . W) . i

hence ((a,x . W) +* m,(a,v . W)) . i = a,v . W by Th12
.= a,((x +* m,v) . m) . W by Th15
.= (a,(x +* m,v) . W) . i by A10, Def11 ;
:: thesis: verum

end;

suppose A11: i <> m ; :: thesis: ((a,x . W) +* m,(a,v . W)) . i = (a,(x +* m,v) . W) . i

hence ((a,x . W) +* m,(a,v . W)) . i = (a,x . W) . i by FUNCT_7:34
.= a,(x . i) . W by Def11
.= a,((x +* m,v) . i) . W by A11, FUNCT_7:34
.= (a,(x +* m,v) . W) . i by Def11 ;
:: thesis: verum

end;

end;

end;

hence (a,x . W) +* m,(a,v . W) = a,(x +* m,v) . W by Th11; :: thesis: verum

end;

( RAS is_semi_additive_in m & *' a,((a,x . W) +* m,(((a,x . W) . m) @ (a,v . W))) = (*' a,(a,x . W)) @ (*' a,((a,x . W) +* m,(a,v . W))) ) by A1, A2, Def8, Th32;
then A12: W . a,(*' a,((a,x . W) +* m,p99m)) = (W . a,(*' a,(a,x . W))) + (W . a,(*' a,((a,x . W) +* m,(a,v . W)))) by A3, Lm6;
Phi x = W . a,(*' a,(a,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 4;
A17: a,(W . a,p) . W = p by Th17;
A18: W . a,p99m = (W . a,(p . m)) + (W . a,p9m) by A16, MIDSP_2:36
.= ((W . a,p) . m) + (W . a,p9m) by Def12 ;
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 Th12
.= a,(((W . a,p) . m) + (W . a,p9m)) . W by A18, MIDSP_2:39
.= a,(((W . a,p) +* m,(((W . a,p) . m) + (W . a,p9m))) . m) . W by Th15
.= (a,((W . a,p) +* m,(((W . a,p) . m) + (W . a,p9m))) . W) . i by A19, Def11 ;
:: 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:34
.= a,((W . a,p) . i) . W by A17, Def11
.= a,(((W . a,p) +* m,(((W . a,p) . m) + (W . a,p9m))) . i) . W by A20, FUNCT_7:34
.= (a,((W . a,p) +* m,(((W . a,p) . m) + (W . a,p9m))) . W) . i by Def11 ;
:: thesis: verum

end;

end;

end;

hence p +* m,p99m = a,((W . a,p) +* m,(((W . a,p) . m) + (W . a,p9m))) . W by Th11; :: 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:39;
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 Th12
.= a,(((W . a,p) +* m,(W . a,p9m)) . m) . W by A22, Th15
.= (a,((W . a,p) +* m,(W . a,p9m)) . W) . i by A23, Def11 ;
:: 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:34
.= a,((W . a,p) . i) . W by A17, Def11
.= a,(((W . a,p) +* m,(W . a,p9m)) . i) . W by A24, FUNCT_7:34
.= (a,((W . a,p) +* m,(W . a,p9m)) . W) . i by Def11 ;
:: thesis: verum

end;

end;

end;

hence p +* m,p9m = a,((W . a,p) +* m,(W . a,p9m)) . W by Th11; :: 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 by Def8; :: thesis: verum

end;