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

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

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

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

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