let n be Nat; :: thesis: for a, b being Real holds (a,b) Subnomial (n + 1) = (a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>
let a, b be Real; :: thesis: (a,b) Subnomial (n + 1) = (a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>
A0: (a,b) Subnomial n is FinSequence of COMPLEX by RVSUM_1:146;
A0a: len ((a,b) Subnomial n) = len (a * ((a,b) Subnomial n)) by COMPLSP2:3;
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,b) Subnomial n)) + (len <*(b |^ (n + 1))*>) by FINSEQ_1:39
.= (len (a * ((a,b) Subnomial n))) + (len <*(b |^ (n + 1))*>) by COMPLSP2:3
.= len ((a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>) 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 * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>) . k

proof

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

per cases ( k in dom ((a,b) Subnomial n) or not k in dom ((a,b) Subnomial n) ) ;

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

then C2: ( 1 <= k & k <= len ((a,b) Subnomial n) ) by FINSEQ_3:25;
then m + 1 <= n + 1 by Def2;
then reconsider l = n - m as Element of NAT by XREAL_1:6, NAT_1:21;
C3: l + 1 = (n + 1) - m ;
k in dom ((a,b) Subnomial (n + 1)) by B0, FINSEQ_3:25;
then ((a,b) Subnomial (n + 1)) . k = (a |^ (l + 1)) * (b |^ m) by Def2, C3
.= (a * (a |^ l)) * (b |^ m) by NEWTON:6
.= a * ((a |^ l) * (b |^ m))
.= a * (((a,b) Subnomial n) . k) by C1, Def2
.= (a * ((a,b) Subnomial n)) . k by A0, COMPLSP2:16
.= ((a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>) . k by A0a, C2, FINSEQ_1:64 ;
hence ((a,b) Subnomial (n + 1)) . k = ((a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>) . k ; :: thesis: verum

end;

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

then not k <= n + 1 by B0, A2, FINSEQ_3:25;
then k >= (n + 1) + 1 by INT_1:7;
then C1: k = (n + 1) + 1 by B0, A2, XXREAL_0:1;
len (a * ((a,b) Subnomial n)) = n + 1 by A2, NEWTON:2;
then ((a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>) . ((n + 1) + 1) = ((a,b) In_Power (n + 1)) . ((n + 1) + 1) by NEWTON:29;
hence ((a,b) Subnomial (n + 1)) . k = ((a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>) . k by NS, C1; :: thesis: verum

end;

end;

end;

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