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

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))
then A3: RAS is_semi_additive_in m by A1, Th32;
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))
consider a being Point of RAS;
set p = a,x . W;
set p'm = a,v . W;
A4: W . a,(a,x . W) = x by Th17;
A5: W . a,(a,v . W) = v by MIDSP_2:39;
consider p''m being Point of RAS such that
A6: p''m @ a = ((a,x . W) . m) @ (a,v . W) by MIDSP_1:def 4;
A7: W . a,p''m = (W . a,((a,x . W) . m)) + (W . a,(a,v . W)) by A6, MIDSP_2:36
.= (x . m) + v by A4, A5, Def12 ;
*' 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 A2, Def8;
then A8: W . a,(*' a,((a,x . W) +* m,p''m)) = (W . a,(*' a,(a,x . W))) + (W . a,(*' a,((a,x . W) +* m,(a,v . W)))) by A3, A6, Lm6;
(a,x . W) +* m,p''m = a,(x +* m,((x . m) + v)) . W

proof

set pp = (a,x . W) +* m,p''m;
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,p''m) . i = (a,(x +* m,((x . m) + v)) . W) . i

proof

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

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

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

hence ((a,x . W) +* m,p''m) . i = p''m by Th12
.= a,((x . m) + v) . W by A7, MIDSP_2:39
.= a,((x +* m,((x . m) + v)) . m) . W by Th15
.= (a,(x +* m,((x . m) + v)) . W) . i by A9, Def11 ;
:: thesis: verum

end;

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

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

end;

end;

end;

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

end;

then A11: Phi (x +* m,((x . m) + v)) = W . a,(*' a,((a,x . W) +* m,p''m)) by Lm5;
A12: Phi x = W . a,(*' a,(a,x . W)) by Lm5;
(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 A13: 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 A13, Def11 ;
:: thesis: verum

end;

suppose A14: 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 A14, 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;

hence Phi (x +* m,((x . m) + v)) = (Phi x) + (Phi (x +* m,v)) by A8, A11, A12, 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 A15: 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 A16: RAS is_semi_additive_in m by Lm7;
for a, pm, p'm being Point of RAS
for p being Tuple of (n + 1),RAS st p . m = pm holds
*' a,(p +* m,(pm @ p'm)) = (*' a,p) @ (*' a,(p +* m,p'm))

proof

let a, pm, p'm be Point of RAS; :: thesis: for p being Tuple of (n + 1),RAS st p . m = pm holds
*' a,(p +* m,(pm @ p'm)) = (*' a,p) @ (*' a,(p +* m,p'm))
let p be Tuple of (n + 1),RAS; :: thesis: ( p . m = pm implies *' a,(p +* m,(pm @ p'm)) = (*' a,p) @ (*' a,(p +* m,p'm)) )
assume A17: p . m = pm ; :: thesis: *' a,(p +* m,(pm @ p'm)) = (*' a,p) @ (*' a,(p +* m,p'm))
set x = W . a,p;
set v = W . a,p'm;
A18: a,(W . a,p) . W = p by Th17;
A19: a,(W . a,p'm) . W = p'm by MIDSP_2:39;
consider p''m being Point of RAS such that
A20: p''m @ a = (p . m) @ p'm by MIDSP_1:def 4;
A21: W . a,p''m = (W . a,(p . m)) + (W . a,p'm) by A20, MIDSP_2:36
.= ((W . a,p) . m) + (W . a,p'm) by Def12 ;
p +* m,p''m = a,((W . a,p) +* m,(((W . a,p) . m) + (W . a,p'm))) . W

proof

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

proof

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

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

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

hence (p +* m,p''m) . i = p''m by Th12
.= a,(((W . a,p) . m) + (W . a,p'm)) . W by A21, MIDSP_2:39
.= a,(((W . a,p) +* m,(((W . a,p) . m) + (W . a,p'm))) . m) . W by Th15
.= (a,((W . a,p) +* m,(((W . a,p) . m) + (W . a,p'm))) . W) . i by A22, Def11 ;
:: thesis: verum

end;

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

hence (p +* m,p''m) . i = p . i by FUNCT_7:34
.= a,((W . a,p) . i) . W by A18, Def11
.= a,(((W . a,p) +* m,(((W . a,p) . m) + (W . a,p'm))) . i) . W by A23, FUNCT_7:34
.= (a,((W . a,p) +* m,(((W . a,p) . m) + (W . a,p'm))) . W) . i by Def11 ;
:: thesis: verum

end;

end;

end;

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

end;

then A24: Phi ((W . a,p) +* m,(((W . a,p) . m) + (W . a,p'm))) = W . a,(*' a,(p +* m,p''m)) by Lm5;
A25: Phi (W . a,p) = W . a,(*' a,p) by Lm4;
p +* m,p'm = a,((W . a,p) +* m,(W . a,p'm)) . W

proof

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

proof

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

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

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

hence (p +* m,p'm) . i = p'm by Th12
.= a,(((W . a,p) +* m,(W . a,p'm)) . m) . W by A19, Th15
.= (a,((W . a,p) +* m,(W . a,p'm)) . W) . i by A26, Def11 ;
:: thesis: verum

end;

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

hence (p +* m,p'm) . i = p . i by FUNCT_7:34
.= a,((W . a,p) . i) . W by A18, Def11
.= a,(((W . a,p) +* m,(W . a,p'm)) . i) . W by A27, FUNCT_7:34
.= (a,((W . a,p) +* m,(W . a,p'm)) . W) . i by Def11 ;
:: thesis: verum

end;

end;

end;

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

end;

then Phi ((W . a,p) +* m,(W . a,p'm)) = W . a,(*' a,(p +* m,p'm)) by Lm5;
then W . a,(*' a,(p +* m,p''m)) = (W . a,(*' a,p)) + (W . a,(*' a,(p +* m,p'm))) by A15, A24, A25;
hence *' a,(p +* m,(pm @ p'm)) = (*' a,p) @ (*' a,(p +* m,p'm)) by A16, A17, A20, Lm6; :: thesis: verum

end;

hence RAS is_additive_in m by Def8; :: thesis: verum

end;