let n be Nat; :: thesis: for m being Nat of n

for RAS being ReperAlgebra of n

for a, b being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b holds

(a,(x +* (m,v))) . W = p +* (m,b)

let m be Nat of n; :: thesis: for RAS being ReperAlgebra of n

for a, b being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b holds

(a,(x +* (m,v))) . W = p +* (m,b)

let RAS be ReperAlgebra of n; :: thesis: for a, b being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b holds

(a,(x +* (m,v))) . W = p +* (m,b)

let a, b be Point of RAS; :: thesis: for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b holds

(a,(x +* (m,v))) . W = p +* (m,b)

let p be Tuple of (n + 1),RAS; :: thesis: for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b holds

(a,(x +* (m,v))) . W = p +* (m,b)

let W be ATLAS of RAS; :: thesis: for v being Vector of W

for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b holds

(a,(x +* (m,v))) . W = p +* (m,b)

let v be Vector of W; :: thesis: for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b holds

(a,(x +* (m,v))) . W = p +* (m,b)

let x be Tuple of (n + 1),W; :: thesis: ( (a,x) . W = p & (a,v) . W = b implies (a,(x +* (m,v))) . W = p +* (m,b) )

assume ( (a,x) . W = p & (a,v) . W = b ) ; :: thesis: (a,(x +* (m,v))) . W = p +* (m,b)

then ( W . (a,p) = x & W . (a,b) = v ) by Th15, MIDSP_2:33;

then W . (a,(p +* (m,b))) = x +* (m,v) by Th25;

hence (a,(x +* (m,v))) . W = p +* (m,b) by Th15; :: thesis: verum

for RAS being ReperAlgebra of n

for a, b being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b holds

(a,(x +* (m,v))) . W = p +* (m,b)

let m be Nat of n; :: thesis: for RAS being ReperAlgebra of n

for a, b being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b holds

(a,(x +* (m,v))) . W = p +* (m,b)

let RAS be ReperAlgebra of n; :: thesis: for a, b being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b holds

(a,(x +* (m,v))) . W = p +* (m,b)

let a, b be Point of RAS; :: thesis: for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b holds

(a,(x +* (m,v))) . W = p +* (m,b)

let p be Tuple of (n + 1),RAS; :: thesis: for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b holds

(a,(x +* (m,v))) . W = p +* (m,b)

let W be ATLAS of RAS; :: thesis: for v being Vector of W

for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b holds

(a,(x +* (m,v))) . W = p +* (m,b)

let v be Vector of W; :: thesis: for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b holds

(a,(x +* (m,v))) . W = p +* (m,b)

let x be Tuple of (n + 1),W; :: thesis: ( (a,x) . W = p & (a,v) . W = b implies (a,(x +* (m,v))) . W = p +* (m,b) )

assume ( (a,x) . W = p & (a,v) . W = b ) ; :: thesis: (a,(x +* (m,v))) . W = p +* (m,b)

then ( W . (a,p) = x & W . (a,b) = v ) by Th15, MIDSP_2:33;

then W . (a,(p +* (m,b))) = x +* (m,v) by Th25;

hence (a,(x +* (m,v))) . W = p +* (m,b) by Th15; :: thesis: verum