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

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

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

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:
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 ; :: thesis: verum
end;
hence RAS is_semi_additive_in m by Th28; :: thesis: verum