let s be Nat; :: thesis: for a, b being Real holds ((a,b) In_Power s) . (s + 1) = b |^ s
let a, b be Real; :: thesis: ((a,b) In_Power s) . (s + 1) = b |^ s
reconsider m1 = (s + 1) - 1 as Element of NAT by INT_1:5, NAT_1:12;
reconsider l1 = s - m1 as Element of NAT by INT_1:5;
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:4;
then ((a,b) In_Power s) . (s + 1) = ((s choose s) * (a |^ l1)) * (b |^ m1) by Def4
.= (1 * (a |^ l1)) * (b |^ m1) by Th21
.= 1 * (b |^ m1) by RVSUM_1:94
.= b |^ s ;
hence ((a,b) In_Power s) . (s + 1) = b |^ s ; :: thesis: verum