let k, n be Nat; ( n > 0 implies (bseq (k + 1)) . n = ((1 / (k + 1)) * ((bseq k) . n)) * ((aseq k) . n) )
assume A1:
n > 0
; (bseq (k + 1)) . n = ((1 / (k + 1)) * ((bseq k) . n)) * ((aseq k) . n)
thus (bseq (k + 1)) . n =
(n choose (k + 1)) * (n ^ (- (k + 1)))
by Def2
.=
(((n - k) / (k + 1)) * (n choose k)) * (n ^ (- (k + 1)))
by Th5
.=
(((n - k) / (k + 1)) * (n choose k)) * ((n ^ (- k)) / n)
by A1, Th4
.=
(((n - k) * ((k + 1) ")) * (n choose k)) * ((n ^ (- k)) / n)
.=
(((n - k) * ((k + 1) ")) * (n choose k)) * ((n ^ (- k)) * (n "))
.=
(((k + 1) ") * ((n choose k) * (n ^ (- k)))) * ((n - k) * (n "))
.=
((1 / (k + 1)) * ((n choose k) * (n ^ (- k)))) * ((n - k) * (n "))
.=
((1 / (k + 1)) * ((n choose k) * (n ^ (- k)))) * ((n - k) / n)
.=
((1 / (k + 1)) * ((bseq k) . n)) * ((n - k) / n)
by Def2
.=
((1 / (k + 1)) * ((bseq k) . n)) * ((aseq k) . n)
by Def1
; verum