let n be 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, Th11;

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

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

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