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) . 1 = a |^ n
let a, b be Element of R; :: thesis: for n being Element of NAT holds (a,b In_Power n) . 1 = a |^ n
let n be Element of NAT ; :: thesis: (a,b In_Power n) . 1 = a |^ n
reconsider m = 1 - 1 as Element of NAT by NEWTON:27;
reconsider l = n - m as Element of NAT ;
len (a,b In_Power n) = n + 1 by Def10;
then A1: dom (a,b In_Power n) = Seg (n + 1) by FINSEQ_1:def 3;
0 + 1 <= n + 1 by XREAL_1:8;
then A2: 1 in dom (a,b In_Power n) by A1, FINSEQ_1:3;
hence (a,b In_Power n) . 1 = (a,b In_Power n) /. 1 by PARTFUN1:def 8
.= ((n choose 0 ) * (a |^ l)) * (b |^ m) by A2, Def10
.= (1 * (a |^ n)) * (b |^ 0 ) by NEWTON:29
.= (a |^ n) * (b |^ 0 ) by Th14
.= (a |^ n) * (1_ R) by Th8
.= a |^ n by GROUP_1:def 5 ;
:: thesis: verum