let n be Nat; :: thesis: for a, b being Real holds (a,b) Subnomial (n + 1) = <*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))
let a, b be Real; :: thesis: (a,b) Subnomial (n + 1) = <*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))
A2: ( len ((a,b) Subnomial (((n + 1) + 1) - 1)) = (n + 1) + 1 & len ((a,b) Subnomial ((n + 1) - 1)) = n + 1 ) ;
then A3: len ((a,b) Subnomial (n + 1)) = (len <*(a |^ (n + 1))*>) + (len ((a,b) Subnomial n)) by FINSEQ_1:39
.= (len <*(a |^ (n + 1))*>) + (len (b * ((a,b) Subnomial n))) by NEWTON:2
.= len (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) by FINSEQ_1:22 ;
for k being Nat st 1 <= k & k <= len ((a,b) Subnomial (n + 1)) holds
((a,b) Subnomial (n + 1)) . k = (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len ((a,b) Subnomial (n + 1)) implies ((a,b) Subnomial (n + 1)) . k = (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . k )
assume B0: ( 1 <= k & k <= len ((a,b) Subnomial (n + 1)) ) ; :: thesis: ((a,b) Subnomial (n + 1)) . k = (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . k

per cases ( k > 1 or k = 1 ) by B0, XXREAL_0:1;

suppose k > 1 ; :: thesis: ((a,b) Subnomial (n + 1)) . k = (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . k

then k >= 1 + 1 by NAT_1:13;
then reconsider m = k - 2 as Element of NAT by NAT_1:21;
C2: n + 2 >= m + 2 by A2, B0;
then reconsider l = n - m as Element of NAT by XREAL_1:6, NAT_1:21;
C3: l = (n + 1) - (m + 1) ;
m <= n by C2, XREAL_1:6;
then C3a: ( 0 + 1 <= m + 1 & m + 1 <= n + 1 ) by XREAL_1:6;
then C4: m + 1 in dom ((a,b) Subnomial n) by A2, FINSEQ_3:25;
C5: ( m = (m + 1) - 1 & l = n - m ) ;
C6: ( 1 <= m + 1 & m + 1 <= len (b * ((a,b) Subnomial n)) ) by C3a, A2, NEWTON:2;
( m + 1 = k - 1 & k in dom ((a,b) Subnomial (n + 1)) ) by B0, FINSEQ_3:25;
then ((a,b) Subnomial (n + 1)) . k = (a |^ l) * (b |^ (m + 1)) by Def2, C3
.= (a |^ l) * (b * (b |^ m)) by NEWTON:6
.= b * ((a |^ l) * (b |^ m))
.= b * (((a,b) Subnomial n) . (m + 1)) by C4, C5, Def2
.= (b * ((a,b) Subnomial n)) . (m + 1) by RVSUM_1:45
.= (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . ((len <*(a |^ (n + 1))*>) + (m + 1)) by C6, FINSEQ_1:65
.= (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . ((m + 1) + 1) by FINSEQ_1:39 ;
hence ((a,b) Subnomial (n + 1)) . k = (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . k ; :: thesis: verum

end;

suppose C1: k = 1 ; :: thesis: ((a,b) Subnomial (n + 1)) . k = (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . k

(<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . 1 = ((a,b) In_Power (n + 1)) . 1 by NEWTON:28;
hence ((a,b) Subnomial (n + 1)) . k = (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . k by NS, C1; :: thesis: verum

end;

end;

end;

hence (a,b) Subnomial (n + 1) = <*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n)) by A3; :: thesis: verum