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

proof

let x be Tuple of (n + 1),W; :: thesis: Phi (x +* m,(Double (x . m))) = Double (Phi x)
set v = x . m;
set y = x +* m,(x . m);
for k being Nat of n holds (x +* m,(x . m)) . k = x . k

proof

let k be Nat of n; :: thesis: (x +* m,(x . m)) . k = x . k

now

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

suppose k = m ; :: thesis: (x +* m,(x . m)) . k = x . k

hence (x +* m,(x . m)) . k = x . k by Th15; :: thesis: verum

end;

suppose k <> m ; :: thesis: (x +* m,(x . m)) . k = x . k

hence (x +* m,(x . m)) . k = x . k by FUNCT_7:34; :: thesis: verum

end;

end;

end;

hence (x +* m,(x . m)) . k = x . k ; :: thesis: verum

end;

then A2: x +* m,(x . m) = x by Th16;
thus Phi (x +* m,(Double (x . m))) = Phi (x +* m,((x . m) + (x . m))) by MIDSP_2:def 1
.= (Phi x) + (Phi (x +* m,(x . m))) by A1
.= Double (Phi x) by A2, MIDSP_2:def 1 ; :: thesis: verum

end;

hence RAS is_semi_additive_in m by Th31; :: thesis: verum