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 W . a,p = x & W . a,b = v holds
W . a,(p +* m,b) = x +* m,v
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 W . a,p = x & W . a,b = v holds
W . a,(p +* m,b) = x +* m,v
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 W . a,p = x & W . a,b = v holds
W . a,(p +* m,b) = x +* m,v
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 W . a,p = x & W . a,b = v holds
W . a,(p +* m,b) = x +* m,v
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 W . a,p = x & W . a,b = v holds
W . a,(p +* m,b) = x +* m,v
let W be ATLAS of RAS; :: thesis: for v being Vector of W
for x being Tuple of (n + 1),W st W . a,p = x & W . a,b = v holds
W . a,(p +* m,b) = x +* m,v
let v be Vector of W; :: thesis: for x being Tuple of (n + 1),W st W . a,p = x & W . a,b = v holds
W . a,(p +* m,b) = x +* m,v
let x be Tuple of (n + 1),W; :: thesis: ( W . a,p = x & W . a,b = v implies W . a,(p +* m,b) = x +* m,v )
assume A1: ( W . a,p = x & W . a,b = v ) ; :: thesis: W . a,(p +* m,b) = x +* m,v
set q = p +* m,b;
set y = W . a,(p +* m,b);
set z = x +* m,v;
for k being Nat of n holds (W . a,(p +* m,b)) . k = (x +* m,v) . k

proof

let k be Nat of n; :: thesis: (W . a,(p +* m,b)) . k = (x +* m,v) . k

now

per cases ( k = m or k <> m ) ;

suppose A2: k = m ; :: thesis: (W . a,(p +* m,b)) . k = (x +* m,v) . k

thus (W . a,(p +* m,b)) . k = W . a,((p +* m,b) . k) by Def12
.= W . a,b by A2, Th12
.= (x +* m,v) . k by A1, A2, Th15 ; :: thesis: verum

end;

suppose A3: k <> m ; :: thesis: (W . a,(p +* m,b)) . k = (x +* m,v) . k

thus (W . a,(p +* m,b)) . k = W . a,((p +* m,b) . k) by Def12
.= W . a,(p . k) by A3, FUNCT_7:34
.= x . k by A1, Def12
.= (x +* m,v) . k by A3, FUNCT_7:34 ; :: thesis: verum

end;

end;

end;

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

end;

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