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)

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

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

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

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

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

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

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