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 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, Th8;

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

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, Th8;

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

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

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

hence
(W . (a,(p +* (m9,(p . m))))) . k = (x +* (m9,(x . m))) . k
; :: thesis: verumper cases
( k = m9 or k <> m9 )
;

end;

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 Def9

.= W . (a,(p . m)) by A3, Th10

.= x . m by A1, Def9

.= (x +* (m9,(x . m))) . k by A3, Th13 ; :: thesis: verum

end;.= W . (a,(p . m)) by A3, Th10

.= x . m by A1, Def9

.= (x +* (m9,(x . m))) . k by A3, Th13 ; :: thesis: verum

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 Def9

.= W . (a,(p . k)) by A4, FUNCT_7:32

.= x . k by A1, Def9

.= (x +* (m9,(x . m))) . k by A4, FUNCT_7:32 ; :: thesis: verum

end;.= W . (a,(p . k)) by A4, FUNCT_7:32

.= x . k by A1, Def9

.= (x +* (m9,(x . m))) . k by A4, FUNCT_7:32 ; :: thesis: verum