let n be Nat; 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; 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; 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; 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; 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; 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; 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; ( (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 )
; (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; verum