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 holds
( RAS is_semi_additive_in m iff for x being Tuple of (n + 1),W holds Phi (x +* m,(Double (x . m))) = Double (Phi x) )
let m be Nat of n; :: thesis: for RAS being ReperAlgebra of n
for W being ATLAS of RAS holds
( RAS is_semi_additive_in m iff for x being Tuple of (n + 1),W holds Phi (x +* m,(Double (x . m))) = Double (Phi x) )
let RAS be ReperAlgebra of n; :: thesis: for W being ATLAS of RAS holds
( RAS is_semi_additive_in m iff for x being Tuple of (n + 1),W holds Phi (x +* m,(Double (x . m))) = Double (Phi x) )
let W be ATLAS of RAS; :: thesis: ( RAS is_semi_additive_in m iff for x being Tuple of (n + 1),W holds Phi (x +* m,(Double (x . m))) = Double (Phi x) )
thus ( RAS is_semi_additive_in m implies for x being Tuple of (n + 1),W holds Phi (x +* m,(Double (x . m))) = Double (Phi x) ) :: thesis: ( ( for x being Tuple of (n + 1),W holds Phi (x +* m,(Double (x . m))) = Double (Phi x) ) implies RAS is_semi_additive_in m )

proof

consider a being Point of RAS;
assume A1: RAS is_semi_additive_in m ; :: thesis: for x being Tuple of (n + 1),W holds Phi (x +* m,(Double (x . m))) = Double (Phi x)
let x be Tuple of (n + 1),W; :: thesis: Phi (x +* m,(Double (x . m))) = Double (Phi x)
set x9 = x +* m,(Double (x . m));
set p = a,x . W;
set p9 = a,(x +* m,(Double (x . m))) . W;
set q = (a,(x +* m,(Double (x . m))) . W) +* m,(a @ ((a,(x +* m,(Double (x . m))) . W) . m));
for i being Nat of n holds (a,x . W) . i = ((a,(x +* m,(Double (x . m))) . W) +* m,(a @ ((a,(x +* m,(Double (x . m))) . W) . m))) . i

proof

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

now

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

suppose A2: i = m ; :: thesis: (a,x . W) . i = ((a,(x +* m,(Double (x . m))) . W) +* m,(a @ ((a,(x +* m,(Double (x . m))) . W) . m))) . i

W . a,(a,x . W) = x by Th17;
then A3: W . a,((a,x . W) . m) = x . m by Def12;
W . a,(a,(x +* m,(Double (x . m))) . W) = x +* m,(Double (x . m)) by Th17;
then A4: W . a,((a,(x +* m,(Double (x . m))) . W) . m) = (x +* m,(Double (x . m))) . m by Def12;
(x +* m,(Double (x . m))) . m = Double (x . m) by Th15;
then (a,x . W) . m = a @ ((a,(x +* m,(Double (x . m))) . W) . m) by A3, A4, MIDSP_2:37
.= ((a,(x +* m,(Double (x . m))) . W) +* m,(a @ ((a,(x +* m,(Double (x . m))) . W) . m))) . m by Th12 ;
hence (a,x . W) . i = ((a,(x +* m,(Double (x . m))) . W) +* m,(a @ ((a,(x +* m,(Double (x . m))) . W) . m))) . i by A2; :: thesis: verum

end;

suppose A5: i <> m ; :: thesis: (a,x . W) . i = ((a,(x +* m,(Double (x . m))) . W) +* m,(a @ ((a,(x +* m,(Double (x . m))) . W) . m))) . i

thus (a,x . W) . i = a,(x . i) . W by Def11
.= a,((x +* m,(Double (x . m))) . i) . W by A5, FUNCT_7:34
.= (a,(x +* m,(Double (x . m))) . W) . i by Def11
.= ((a,(x +* m,(Double (x . m))) . W) +* m,(a @ ((a,(x +* m,(Double (x . m))) . W) . m))) . i by A5, FUNCT_7:34 ; :: thesis: verum

end;

end;

end;

hence (a,x . W) . i = ((a,(x +* m,(Double (x . m))) . W) +* m,(a @ ((a,(x +* m,(Double (x . m))) . W) . m))) . i ; :: thesis: verum

end;

then a,x . W = (a,(x +* m,(Double (x . m))) . W) +* m,(a @ ((a,(x +* m,(Double (x . m))) . W) . m)) by Th11;
then *' a,(a,x . W) = a @ (*' a,(a,(x +* m,(Double (x . m))) . W)) by A1, Def7;
then A6: W . a,(*' a,(a,(x +* m,(Double (x . m))) . W)) = Double (W . a,(*' a,(a,x . W))) by MIDSP_2:37;
Phi (x +* m,(Double (x . m))) = W . a,(*' a,(a,(x +* m,(Double (x . m))) . W)) by Lm5;
hence Phi (x +* m,(Double (x . m))) = Double (Phi x) by A6, Lm5; :: thesis: verum

end;

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

proof

assume A7: for x being Tuple of (n + 1),W holds Phi (x +* m,(Double (x . m))) = Double (Phi x) ; :: 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 p9m be Point of RAS; :: thesis: for p being Tuple of (n + 1),RAS st p . m = p9m holds
*' a,(p +* m,(a @ p9m)) = a @ (*' a,p)
let p9 be Tuple of (n + 1),RAS; :: thesis: ( p9 . m = p9m implies *' a,(p9 +* m,(a @ p9m)) = a @ (*' a,p9) )
assume A8: p9 . m = p9m ; :: thesis: *' a,(p9 +* m,(a @ p9m)) = a @ (*' a,p9)
set p = p9 +* m,(a @ (p9 . m));
set x = W . a,(p9 +* m,(a @ (p9 . m)));
set x9 = (W . a,(p9 +* m,(a @ (p9 . m)))) +* m,(Double ((W . a,(p9 +* m,(a @ (p9 . m)))) . m));
W . a,p9 = (W . a,(p9 +* m,(a @ (p9 . m)))) +* m,(Double ((W . a,(p9 +* m,(a @ (p9 . m)))) . m))

proof

set y = W . a,p9;
for i being Nat of n holds ((W . a,(p9 +* m,(a @ (p9 . m)))) +* m,(Double ((W . a,(p9 +* m,(a @ (p9 . m)))) . m))) . i = (W . a,p9) . i

proof

let i be Nat of n; :: thesis: ((W . a,(p9 +* m,(a @ (p9 . m)))) +* m,(Double ((W . a,(p9 +* m,(a @ (p9 . m)))) . m))) . i = (W . a,p9) . i

now

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

suppose A9: i = m ; :: thesis: ((W . a,(p9 +* m,(a @ (p9 . m)))) +* m,(Double ((W . a,(p9 +* m,(a @ (p9 . m)))) . m))) . i = (W . a,p9) . i

A10: ( W . a,((p9 +* m,(a @ (p9 . m))) . m) = (W . a,(p9 +* m,(a @ (p9 . m)))) . m & (p9 +* m,(a @ (p9 . m))) . m = a @ (p9 . m) ) by Def12, Th12;
( ((W . a,(p9 +* m,(a @ (p9 . m)))) +* m,(Double ((W . a,(p9 +* m,(a @ (p9 . m)))) . m))) . m = Double ((W . a,(p9 +* m,(a @ (p9 . m)))) . m) & W . a,(p9 . m) = (W . a,p9) . m ) by Def12, Th15;
hence ((W . a,(p9 +* m,(a @ (p9 . m)))) +* m,(Double ((W . a,(p9 +* m,(a @ (p9 . m)))) . m))) . i = (W . a,p9) . i by A9, A10, MIDSP_2:37; :: thesis: verum

end;

suppose A11: i <> m ; :: thesis: ((W . a,(p9 +* m,(a @ (p9 . m)))) +* m,(Double ((W . a,(p9 +* m,(a @ (p9 . m)))) . m))) . i = (W . a,p9) . i

hence ((W . a,(p9 +* m,(a @ (p9 . m)))) +* m,(Double ((W . a,(p9 +* m,(a @ (p9 . m)))) . m))) . i = (W . a,(p9 +* m,(a @ (p9 . m)))) . i by FUNCT_7:34
.= W . a,((p9 +* m,(a @ (p9 . m))) . i) by Def12
.= W . a,(p9 . i) by A11, FUNCT_7:34
.= (W . a,p9) . i by Def12 ;
:: thesis: verum

end;

end;

end;

hence ((W . a,(p9 +* m,(a @ (p9 . m)))) +* m,(Double ((W . a,(p9 +* m,(a @ (p9 . m)))) . m))) . i = (W . a,p9) . i ; :: thesis: verum

end;

hence W . a,p9 = (W . a,(p9 +* m,(a @ (p9 . m)))) +* m,(Double ((W . a,(p9 +* m,(a @ (p9 . m)))) . m)) by Th16; :: thesis: verum

end;

then A12: Phi ((W . a,(p9 +* m,(a @ (p9 . m)))) +* m,(Double ((W . a,(p9 +* m,(a @ (p9 . m)))) . m))) = W . a,(*' a,p9) by Lm4;
Phi (W . a,(p9 +* m,(a @ (p9 . m)))) = W . a,(*' a,(p9 +* m,(a @ (p9 . m)))) by Lm4;
then W . a,(*' a,p9) = Double (W . a,(*' a,(p9 +* m,(a @ (p9 . m))))) by A7, A12;
hence *' a,(p9 +* m,(a @ p9m)) = a @ (*' a,p9) by A8, MIDSP_2:37; :: thesis: verum

end;