let n be 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 )

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

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
set a = the 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 = ( the Point of RAS,x) . W;

set p9 = ( the Point of RAS,(x +* (m,(Double (x . m))))) . W;

set q = (( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)));

for i being Nat of n holds (( the Point of RAS,x) . W) . i = ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . i

then *' ( the Point of RAS,(( the Point of RAS,x) . W)) = the Point of RAS @ (*' ( the Point of RAS,(( the Point of RAS,(x +* (m,(Double (x . m))))) . W))) by A1;

then A6: W . ( the Point of RAS,(*' ( the Point of RAS,(( the Point of RAS,(x +* (m,(Double (x . m))))) . W)))) = Double (W . ( the Point of RAS,(*' ( the Point of RAS,(( the Point of RAS,x) . W))))) by MIDSP_2:31;

Phi (x +* (m,(Double (x . m)))) = W . ( the Point of RAS,(*' ( the Point of RAS,(( the Point of RAS,(x +* (m,(Double (x . m))))) . W)))) by Lm5;

hence Phi (x +* (m,(Double (x . m)))) = Double (Phi x) by A6, Lm5; :: thesis: verum

end;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 = ( the Point of RAS,x) . W;

set p9 = ( the Point of RAS,(x +* (m,(Double (x . m))))) . W;

set q = (( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)));

for i being Nat of n holds (( the Point of RAS,x) . W) . i = ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . i

proof

then
( the Point of RAS,x) . W = (( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))
by Th9;
let i be Nat of n; :: thesis: (( the Point of RAS,x) . W) . i = ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . i

end;now :: thesis: (( the Point of RAS,x) . W) . i = ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . iend;

hence
(( the Point of RAS,x) . W) . i = ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . i
; :: thesis: verumper cases
( i = m or i <> m )
;

end;

suppose A2:
i = m
; :: thesis: (( the Point of RAS,x) . W) . i = ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . i

W . ( the Point of RAS,(( the Point of RAS,x) . W)) = x
by Th15;

then A3: W . ( the Point of RAS,((( the Point of RAS,x) . W) . m)) = x . m by Def9;

W . ( the Point of RAS,(( the Point of RAS,(x +* (m,(Double (x . m))))) . W)) = x +* (m,(Double (x . m))) by Th15;

then A4: W . ( the Point of RAS,((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)) = (x +* (m,(Double (x . m)))) . m by Def9;

(x +* (m,(Double (x . m)))) . m = Double (x . m) by Th13;

then (( the Point of RAS,x) . W) . m = the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m) by A3, A4, MIDSP_2:31

.= ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . m by Th10 ;

hence (( the Point of RAS,x) . W) . i = ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . i by A2; :: thesis: verum

end;then A3: W . ( the Point of RAS,((( the Point of RAS,x) . W) . m)) = x . m by Def9;

W . ( the Point of RAS,(( the Point of RAS,(x +* (m,(Double (x . m))))) . W)) = x +* (m,(Double (x . m))) by Th15;

then A4: W . ( the Point of RAS,((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)) = (x +* (m,(Double (x . m)))) . m by Def9;

(x +* (m,(Double (x . m)))) . m = Double (x . m) by Th13;

then (( the Point of RAS,x) . W) . m = the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m) by A3, A4, MIDSP_2:31

.= ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . m by Th10 ;

hence (( the Point of RAS,x) . W) . i = ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . i by A2; :: thesis: verum

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

thus (( the Point of RAS,x) . W) . i =
( the Point of RAS,(x . i)) . W
by Def8

.= ( the Point of RAS,((x +* (m,(Double (x . m)))) . i)) . W by A5, FUNCT_7:32

.= (( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . i by Def8

.= ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . i by A5, FUNCT_7:32 ; :: thesis: verum

end;.= ( the Point of RAS,((x +* (m,(Double (x . m)))) . i)) . W by A5, FUNCT_7:32

.= (( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . i by Def8

.= ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . i by A5, FUNCT_7:32 ; :: thesis: verum

then *' ( the Point of RAS,(( the Point of RAS,x) . W)) = the Point of RAS @ (*' ( the Point of RAS,(( the Point of RAS,(x +* (m,(Double (x . m))))) . W))) by A1;

then A6: W . ( the Point of RAS,(*' ( the Point of RAS,(( the Point of RAS,(x +* (m,(Double (x . m))))) . W)))) = Double (W . ( the Point of RAS,(*' ( the Point of RAS,(( the Point of RAS,x) . W))))) by MIDSP_2:31;

Phi (x +* (m,(Double (x . m)))) = W . ( the Point of RAS,(*' ( the Point of RAS,(( the Point of RAS,(x +* (m,(Double (x . m))))) . W)))) by Lm5;

hence Phi (x +* (m,(Double (x . m)))) = Double (Phi x) by A6, Lm5; :: 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 5 :: 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)))

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:31; :: thesis: verum

end;let a be Point of RAS; :: according to MIDSP_3:def 5 :: 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

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;
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

end;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

hence
W . (a,p9) = (W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)))
by Th14; :: thesis: verum
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

end;now :: thesis: ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)))) . i = (W . (a,p9)) . iend;

hence
((W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)))) . i = (W . (a,p9)) . i
; :: thesis: verumper cases
( i = m or i <> m )
;

end;

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 Def9, Th10;

( ((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 Def9, Th13;

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:31; :: thesis: verum

end;( ((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 Def9, Th13;

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:31; :: thesis: verum

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:32

.= W . (a,((p9 +* (m,(a @ (p9 . m)))) . i)) by Def9

.= W . (a,(p9 . i)) by A11, FUNCT_7:32

.= (W . (a,p9)) . i by Def9 ;

:: thesis: verum

end;.= W . (a,((p9 +* (m,(a @ (p9 . m)))) . i)) by Def9

.= W . (a,(p9 . i)) by A11, FUNCT_7:32

.= (W . (a,p9)) . i by Def9 ;

:: thesis: verum

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:31; :: thesis: verum