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 RAS is_semi_additive_in m holds
for a, p9m, p99m being Point of RAS
for p being Tuple of (n + 1),RAS st a @ p99m = (p . m) @ p9m holds
( *' a,(p +* m,((p . m) @ p9m)) = (*' a,p) @ (*' a,(p +* m,p9m)) iff W . a,(*' a,(p +* m,p99m)) = (W . a,(*' a,p)) + (W . a,(*' a,(p +* m,p9m))) )
let m be Nat of n; :: thesis: for RAS being ReperAlgebra of n
for W being ATLAS of RAS st RAS is_semi_additive_in m holds
for a, p9m, p99m being Point of RAS
for p being Tuple of (n + 1),RAS st a @ p99m = (p . m) @ p9m holds
( *' a,(p +* m,((p . m) @ p9m)) = (*' a,p) @ (*' a,(p +* m,p9m)) iff W . a,(*' a,(p +* m,p99m)) = (W . a,(*' a,p)) + (W . a,(*' a,(p +* m,p9m))) )
let RAS be ReperAlgebra of n; :: thesis: for W being ATLAS of RAS st RAS is_semi_additive_in m holds
for a, p9m, p99m being Point of RAS
for p being Tuple of (n + 1),RAS st a @ p99m = (p . m) @ p9m holds
( *' a,(p +* m,((p . m) @ p9m)) = (*' a,p) @ (*' a,(p +* m,p9m)) iff W . a,(*' a,(p +* m,p99m)) = (W . a,(*' a,p)) + (W . a,(*' a,(p +* m,p9m))) )
let W be ATLAS of RAS; :: thesis: ( RAS is_semi_additive_in m implies for a, p9m, p99m being Point of RAS
for p being Tuple of (n + 1),RAS st a @ p99m = (p . m) @ p9m holds
( *' a,(p +* m,((p . m) @ p9m)) = (*' a,p) @ (*' a,(p +* m,p9m)) iff W . a,(*' a,(p +* m,p99m)) = (W . a,(*' a,p)) + (W . a,(*' a,(p +* m,p9m))) ) )
assume A1: RAS is_semi_additive_in m ; :: thesis: for a, p9m, p99m being Point of RAS
for p being Tuple of (n + 1),RAS st a @ p99m = (p . m) @ p9m holds
( *' a,(p +* m,((p . m) @ p9m)) = (*' a,p) @ (*' a,(p +* m,p9m)) iff W . a,(*' a,(p +* m,p99m)) = (W . a,(*' a,p)) + (W . a,(*' a,(p +* m,p9m))) )
let a, p9m, p99m be Point of RAS; :: thesis: for p being Tuple of (n + 1),RAS st a @ p99m = (p . m) @ p9m holds
( *' a,(p +* m,((p . m) @ p9m)) = (*' a,p) @ (*' a,(p +* m,p9m)) iff W . a,(*' a,(p +* m,p99m)) = (W . a,(*' a,p)) + (W . a,(*' a,(p +* m,p9m))) )
let p be Tuple of (n + 1),RAS; :: thesis: ( a @ p99m = (p . m) @ p9m implies ( *' a,(p +* m,((p . m) @ p9m)) = (*' a,p) @ (*' a,(p +* m,p9m)) iff W . a,(*' a,(p +* m,p99m)) = (W . a,(*' a,p)) + (W . a,(*' a,(p +* m,p9m))) ) )
assume a @ p99m = (p . m) @ p9m ; :: thesis: ( *' a,(p +* m,((p . m) @ p9m)) = (*' a,p) @ (*' a,(p +* m,p9m)) iff W . a,(*' a,(p +* m,p99m)) = (W . a,(*' a,p)) + (W . a,(*' a,(p +* m,p9m))) )
then *' a,(p +* m,((p . m) @ p9m)) = a @ (*' a,(p +* m,p99m)) by A1, Th13;
hence ( *' a,(p +* m,((p . m) @ p9m)) = (*' a,p) @ (*' a,(p +* m,p9m)) iff W . a,(*' a,(p +* m,p99m)) = (W . a,(*' a,p)) + (W . a,(*' a,(p +* m,p9m))) ) by MIDSP_2:36; :: thesis: verum