let n be Element of 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 Th17, MIDSP_2:39;
then W . a,(p +* m,b) = x +* m,v by Th28;
hence a,(x +* m,v) . W = p +* m,b by Th17; :: thesis: verum