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