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

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)
consider a being Point of RAS;
set x' = x +* m,(Double (x . m));
set p = a,x . W;
set p' = 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

A3: (x +* m,(Double (x . m))) . m = Double (x . m) by Th15;
( W . a,(a,x . W) = x & W . a,(a,(x +* m,(Double (x . m))) . W) = x +* m,(Double (x . m)) ) by Th17;
then ( W . a,((a,x . W) . m) = x . m & W . a,((a,(x +* m,(Double (x . m))) . W) . m) = (x +* m,(Double (x . m))) . m ) by Def12;
then (a,x . W) . m = a @ ((a,(x +* m,(Double (x . m))) . W) . m) by A3, 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 A4: 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 A4, 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 A4, 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 A5: 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 A5, 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 A6: 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 p'm be Point of RAS; :: thesis: for p being Tuple of (n + 1),RAS st p . m = p'm holds
*' a,(p +* m,(a @ p'm)) = a @ (*' a,p)
let p' be Tuple of (n + 1),RAS; :: thesis: ( p' . m = p'm implies *' a,(p' +* m,(a @ p'm)) = a @ (*' a,p') )
assume A7: p' . m = p'm ; :: thesis: *' a,(p' +* m,(a @ p'm)) = a @ (*' a,p')
set p = p' +* m,(a @ (p' . m));
set x = W . a,(p' +* m,(a @ (p' . m)));
set x' = (W . a,(p' +* m,(a @ (p' . m)))) +* m,(Double ((W . a,(p' +* m,(a @ (p' . m)))) . m));
W . a,p' = (W . a,(p' +* m,(a @ (p' . m)))) +* m,(Double ((W . a,(p' +* m,(a @ (p' . m)))) . m))

proof

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

proof

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

now

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

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

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

end;

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

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

end;

end;

end;

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

end;

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

end;

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

end;