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 W . a,p = x & m <= n holds
W . a,(p +* (m + 1),(p . m)) = x +* (m + 1),(x . 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 W . a,p = x & m <= n holds
W . a,(p +* (m + 1),(p . m)) = x +* (m + 1),(x . 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 W . a,p = x & m <= n holds
W . a,(p +* (m + 1),(p . m)) = x +* (m + 1),(x . 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 W . a,p = x & m <= n holds
W . a,(p +* (m + 1),(p . m)) = x +* (m + 1),(x . 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 W . a,p = x & m <= n holds
W . a,(p +* (m + 1),(p . m)) = x +* (m + 1),(x . m)
let W be ATLAS of RAS; :: thesis: for x being Tuple of (n + 1),W st W . a,p = x & m <= n holds
W . a,(p +* (m + 1),(p . m)) = x +* (m + 1),(x . m)
let x be Tuple of (n + 1),W; :: thesis: ( W . a,p = x & m <= n implies W . a,(p +* (m + 1),(p . m)) = x +* (m + 1),(x . m) )
assume that
A1: W . a,p = x and
A2: m <= n ; :: thesis: W . a,(p +* (m + 1),(p . m)) = x +* (m + 1),(x . m)
reconsider m9 = m + 1 as Nat of n by A2, Th10;
set y = W . a,(p +* m9,(p . m));
set z = x +* m9,(x . m);
for k being Nat of n holds (W . a,(p +* m9,(p . m))) . k = (x +* m9,(x . m)) . k

proof

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

now

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

suppose A3: k = m9 ; :: thesis: (W . a,(p +* m9,(p . m))) . k = (x +* m9,(x . m)) . k

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

end;

suppose A4: k <> m9 ; :: thesis: (W . a,(p +* m9,(p . m))) . k = (x +* m9,(x . m)) . k

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

end;

end;

end;

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

end;

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