let s be Nat; :: thesis: for a, b being real number holds (a,b In_Power s) . (s + 1) = b |^ s
let a, b be real number ; :: thesis: (a,b In_Power s) . (s + 1) = b |^ s
reconsider m1 = (s + 1) - 1 as Element of NAT by INT_1:18, NAT_1:12;
reconsider l1 = s - m1 as Element of NAT by INT_1:18;
len (a,b In_Power s) = s + 1 by Def4;
then dom (a,b In_Power s) = Seg (s + 1) by FINSEQ_1:def 3;
then s + 1 in dom (a,b In_Power s) by FINSEQ_1:6;
then (a,b In_Power s) . (s + 1) = ((s choose s) * (a |^ l1)) * (b |^ m1) by Def4
.= (1 * (a |^ l1)) * (b |^ m1) by Th31
.= 1 * (b |^ m1) by RVSUM_1:124
.= b |^ s ;
hence (a,b In_Power s) . (s + 1) = b |^ s ; :: thesis: verum