let a, b be Real; for n being Nat holds (a,b) Subnomial (n + 2) = (<*(a |^ (n + 2))*> ^ ((a * b) * ((a,b) Subnomial n))) ^ <*(b |^ (n + 2))*>
let n be Nat; (a,b) Subnomial (n + 2) = (<*(a |^ (n + 2))*> ^ ((a * b) * ((a,b) Subnomial n))) ^ <*(b |^ (n + 2))*>
reconsider f = (b,a) Subnomial n as complex-valued FinSequence ;
A0: Rev ((b,a) Subnomial (n + 1)) =
Rev (<*(b |^ (n + 1))*> ^ (a * ((b,a) Subnomial n)))
by SAN
.=
(Rev (a * ((b,a) Subnomial n))) ^ (Rev <*(b |^ (n + 1))*>)
by FINSEQ_5:64
.=
(a * (Rev ((b,a) Subnomial n))) ^ (Rev <*(b |^ (n + 1))*>)
by CREV
.=
(a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>
by SAB
;
(a,b) Subnomial ((n + 1) + 1) =
<*(a |^ (n + 2))*> ^ (b * ((a,b) Subnomial (n + 1)))
by SAN
.=
<*(a |^ (n + 2))*> ^ (b * (Rev ((b,a) Subnomial (n + 1))))
by SAB
.=
<*(a |^ (n + 2))*> ^ ((b * (a * ((a,b) Subnomial n))) ^ (b * <*(b |^ (n + 1))*>))
by A0, ADP
.=
(<*(a |^ (n + 2))*> ^ (b * (a * ((a,b) Subnomial n)))) ^ (b * <*(b |^ (n + 1))*>)
by FINSEQ_1:32
.=
(<*(a |^ (n + 2))*> ^ (b * (a * ((a,b) Subnomial n)))) ^ <*(b * (b |^ (n + 1)))*>
by AMP
.=
(<*(a |^ (n + 2))*> ^ (b * (a * ((a,b) Subnomial n)))) ^ <*(b |^ ((n + 1) + 1))*>
by NEWTON:6
.=
(<*(a |^ (n + 2))*> ^ ((b * a) * ((a,b) Subnomial n))) ^ <*(b |^ ((n + 1) + 1))*>
by VALUED_2:16
;
hence
(a,b) Subnomial (n + 2) = (<*(a |^ (n + 2))*> ^ ((a * b) * ((a,b) Subnomial n))) ^ <*(b |^ (n + 2))*>
; verum