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 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 that
A1: W . (a,p) = x and
A2: 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 :: thesis: (W . (a,(p +* (m,b)))) . k = (x +* (m,v)) . k

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

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 Def9
.= W . (a,b) by A3, Th10
.= (x +* (m,v)) . k by A2, A3, Th13 ; :: thesis: verum

end;

suppose A4: 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 Def9
.= W . (a,(p . k)) by A4, FUNCT_7:32
.= x . k by A1, Def9
.= (x +* (m,v)) . k by A4, FUNCT_7:32 ; :: 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 Th14; :: thesis: verum