let n be 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 :: thesis: (x +* (m,(x . m))) . k = x . k

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

end;

end;

end;

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

end;

then A2: x +* (m,(x . m)) = x by Th14;
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 Th28; :: thesis: verum