let a, b be Real; :: thesis: for n being Nat holds (a,b) Subnomial (n + 1) = <*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))
let n be Nat; :: thesis: (a,b) Subnomial (n + 1) = <*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))
A0: dom ((a,b) Subnomial n) = dom (b * ((a,b) Subnomial n)) by VALUED_1:def 5;
A1: dom ((a,b) Subnomial (n + 1)) = dom (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n)))

proof

len ((a,b) Subnomial (((n + 1) + 1) - 1)) = 1 + (len ((a,b) Subnomial ((n + 1) - 1)))
.= (1 * (len <*(a |^ (n + 1))*>)) + (len ((a,b) Subnomial n))
.= (len <*(a |^ (n + 1))*>) + (len (b * ((a,b) Subnomial n))) by A0, FINSEQ_3:29
.= len (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) by FINSEQ_1:22 ;
hence dom ((a,b) Subnomial (n + 1)) = dom (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) by FINSEQ_3:29; :: thesis: verum

end;

for i being object st i in dom ((a,b) Subnomial (n + 1)) holds
((a,b) Subnomial (n + 1)) . i = (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . i

proof

let i be object ; :: thesis: ( i in dom ((a,b) Subnomial (n + 1)) implies ((a,b) Subnomial (n + 1)) . i = (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . i )
assume B1: i in dom ((a,b) Subnomial (n + 1)) ; :: thesis: ((a,b) Subnomial (n + 1)) . i = (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . i
reconsider i = i as non zero Nat by B1, FINSEQ_3:25;
B2: ( 1 <= i & i <= len ((a,b) Subnomial (((n + 1) + 1) - 1)) ) by B1, FINSEQ_3:25;
reconsider j = i - 1 as Nat ;
B3: j + 1 <= (n + 1) + 1 by B2;
then ex k being Nat st n + 1 = j + k by XREAL_1:6, NAT_1:10;
then reconsider k = (n + 1) - j as Nat ;
set m = n + 1;

per cases ( j = 0 or j > 0 ) ;

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

then C2: ( (len ((a,b) Subnomial (((n + 1) + 1) - 1))) - 1 = n + 1 & j = 1 - 1 & (n + 1) - j = n + 1 ) ;
1 + 0 <= 1 + (n + 1) by XREAL_1:6;
then 1 <= len ((a,b) Subnomial (((n + 1) + 1) - 1)) ;
then 1 in dom ((a,b) Subnomial (n + 1)) by FINSEQ_3:25;
then ((a,b) Subnomial (n + 1)) . 1 = (a |^ (n + 1)) * (1 * (b |^ 0)) by C2, Def2
.= (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . 1 ;
hence ((a,b) Subnomial (n + 1)) . i = (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . i by C1; :: thesis: verum

end;

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

then ( len ((a,b) Subnomial ((n + 1) - 1)) >= j & j >= 0 + 1 ) by B3, XREAL_1:6, NAT_1:13;
then C1: j in dom ((a,b) Subnomial ((n + 1) - 1)) by FINSEQ_3:25;
then C2: j in dom (b * ((a,b) Subnomial ((n + 1) - 1))) by VALUED_1:def 5;
then C3: ( len (b * ((a,b) Subnomial ((n + 1) - 1))) >= j & j >= 1 ) by FINSEQ_3:25;
reconsider x = j - 1 as Nat by C0;
C5: ( n = x + k & k = n - x ) ;
1 * (len <*(a |^ (n + 1))*>) = 1 ;
then (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . (1 + j) = (b * ((a,b) Subnomial n)) . j by C3, FINSEQ_1:65
.= b * (((a,b) Subnomial ((n + 1) - 1)) . j) by C2, VALUED_1:def 5
.= b * ((a |^ k) * (b |^ x)) by C1, C5, Def2
.= (a |^ k) * (b * (b |^ x))
.= (a |^ k) * (b |^ (x + 1)) by NEWTON:6
.= ((a,b) Subnomial (((n + 1) + 1) - 1)) . i by B1, Def2 ;
hence ((a,b) Subnomial (n + 1)) . i = (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . i ; :: thesis: verum

end;

end;

end;

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