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