reconsider m = 1 - 1 as Element of NAT by NEWTON:19;
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) . 1 = a |^ n
let a, b be Element of R; for n being Nat holds ((a,b) In_Power n) . 1 = a |^ n
let n be Nat; ((a,b) In_Power n) . 1 = a |^ n
reconsider l = n - m as Nat ;
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;
0 + 1 <= n + 1
by XREAL_1:6;
then A2:
1 in dom ((a,b) In_Power n)
by A1, FINSEQ_1:1;
hence ((a,b) In_Power n) . 1 =
((a,b) In_Power n) /. 1
by PARTFUN1:def 6
.=
((n choose 0) * (a |^ l)) * (b |^ m)
by A2, Def7
.=
(1 * (a |^ n)) * (b |^ 0)
by NEWTON:19
.=
(a |^ n) * (b |^ 0)
by Th13
.=
(a |^ n) * (1_ R)
by Th8
.=
a |^ n
by GROUP_1:def 4
;
verum