let a, b be Real; :: thesis: for s being natural Number holds ((a,b) In_Power s) . 1 = a |^ s
let s be natural Number ; :: thesis: ((a,b) In_Power s) . 1 = a |^ s
reconsider m1 = 1 - 1 as Element of NAT by INT_1:5;
reconsider l1 = s - m1 as Nat ;
len ((a,b) In_Power s) = s + 1 by Def4;
then A1: dom ((a,b) In_Power s) = Seg (s + 1) by FINSEQ_1:def 3;
s + 1 >= 0 + 1 by XREAL_1:6;
then 1 in dom ((a,b) In_Power s) by A1;
then ((a,b) In_Power s) . 1 = ((s choose 0) * (a |^ l1)) * (b |^ m1) by Def4
.= (1 * (a |^ l1)) * (b |^ m1) by Th19
.= a |^ s by RVSUM_1:94 ;
hence ((a,b) In_Power s) . 1 = a |^ s ; :: thesis: verum