let R be non empty unital right_zeroed doubleLoopStr ; for a, b being Element of R
for n being Nat holds ((a,b) In_Power n) . (n + 1) = b |^ n
let a, b be Element of R; for n being Nat holds ((a,b) In_Power n) . (n + 1) = b |^ n
let n be Nat; ((a,b) In_Power n) . (n + 1) = b |^ n
reconsider m = (n + 1) - 1 as Nat ;
reconsider l = n - m as Element of NAT by INT_1:5;
len ((a,b) In_Power n) = n + 1
by Def7;
then A1:
dom ((a,b) In_Power n) = Seg (n + 1)
by FINSEQ_1:def 3;
then A2:
( l = 0 & n + 1 in dom ((a,b) In_Power n) )
by FINSEQ_1:4;
thus ((a,b) In_Power n) . (n + 1) =
((a,b) In_Power n) /. (n + 1)
by A1, FINSEQ_1:4, PARTFUN1:def 6
.=
((n choose n) * (a |^ 0)) * (b |^ n)
by A2, Def7
.=
(1 * (a |^ 0)) * (b |^ n)
by NEWTON:21
.=
(1 * (1_ R)) * (b |^ n)
by Th8
.=
(1_ R) * (b |^ n)
by Th13
.=
b |^ n
by GROUP_1:def 4
; verum