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