let n be Nat; :: thesis: for m being Nat of n

for RAS being ReperAlgebra of n

for a being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for x being Tuple of (n + 1),W st (a,x) . W = p & m <= n holds

(a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m))

let m be Nat of n; :: thesis: for RAS being ReperAlgebra of n

for a being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for x being Tuple of (n + 1),W st (a,x) . W = p & m <= n holds

(a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m))

let RAS be ReperAlgebra of n; :: thesis: for a being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for x being Tuple of (n + 1),W st (a,x) . W = p & m <= n holds

(a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m))

let a be Point of RAS; :: thesis: for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for x being Tuple of (n + 1),W st (a,x) . W = p & m <= n holds

(a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m))

let p be Tuple of (n + 1),RAS; :: thesis: for W being ATLAS of RAS

for x being Tuple of (n + 1),W st (a,x) . W = p & m <= n holds

(a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m))

let W be ATLAS of RAS; :: thesis: for x being Tuple of (n + 1),W st (a,x) . W = p & m <= n holds

(a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m))

let x be Tuple of (n + 1),W; :: thesis: ( (a,x) . W = p & m <= n implies (a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m)) )

assume that

A1: (a,x) . W = p and

A2: m <= n ; :: thesis: (a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m))

W . (a,p) = x by A1, Th15;

then W . (a,(p +* ((m + 1),(p . m)))) = x +* ((m + 1),(x . m)) by A2, Th31;

hence (a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m)) by Th15; :: thesis: verum

for RAS being ReperAlgebra of n

for a being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for x being Tuple of (n + 1),W st (a,x) . W = p & m <= n holds

(a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m))

let m be Nat of n; :: thesis: for RAS being ReperAlgebra of n

for a being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for x being Tuple of (n + 1),W st (a,x) . W = p & m <= n holds

(a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m))

let RAS be ReperAlgebra of n; :: thesis: for a being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for x being Tuple of (n + 1),W st (a,x) . W = p & m <= n holds

(a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m))

let a be Point of RAS; :: thesis: for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for x being Tuple of (n + 1),W st (a,x) . W = p & m <= n holds

(a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m))

let p be Tuple of (n + 1),RAS; :: thesis: for W being ATLAS of RAS

for x being Tuple of (n + 1),W st (a,x) . W = p & m <= n holds

(a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m))

let W be ATLAS of RAS; :: thesis: for x being Tuple of (n + 1),W st (a,x) . W = p & m <= n holds

(a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m))

let x be Tuple of (n + 1),W; :: thesis: ( (a,x) . W = p & m <= n implies (a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m)) )

assume that

A1: (a,x) . W = p and

A2: m <= n ; :: thesis: (a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m))

W . (a,p) = x by A1, Th15;

then W . (a,(p +* ((m + 1),(p . m)))) = x +* ((m + 1),(x . m)) by A2, Th31;

hence (a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m)) by Th15; :: thesis: verum