let a, b be Real; :: thesis: for n, i being Nat holds ((a,b) Subnomial n) . i <= ((|.a.|,|.b.|) Subnomial n) . i
let n, i be Nat; :: thesis: ((a,b) Subnomial n) . i <= ((|.a.|,|.b.|) Subnomial n) . i
reconsider f = (|.a.|,|.b.|) Subnomial n as nonnegative-yielding FinSequence of REAL ;

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

suppose not i in dom ((a,b) Subnomial n) ; :: thesis: ((a,b) Subnomial n) . i <= ((|.a.|,|.b.|) Subnomial n) . i

hence ((a,b) Subnomial n) . i <= ((|.a.|,|.b.|) Subnomial n) . i by FUNCT_1:def 2; :: thesis: verum

end;

suppose A0: i in dom ((a,b) Subnomial n) ; :: thesis: ((a,b) Subnomial n) . i <= ((|.a.|,|.b.|) Subnomial n) . i

then A1: ( 1 <= i & i <= len ((a,b) Subnomial ((n + 1) - 1)) ) by FINSEQ_3:25;
then reconsider l = i - 1 as Nat ;
ex k being Nat st n + 1 = (l + 1) + k by A1, NAT_1:10;
then reconsider k = (n + 1) - (l + 1) as Nat ;
A2: ( k = n - l & l = i - 1 ) ;
A3: ( |.a.| |^ k = |.(a |^ k).| & |.b.| |^ l = |.(b |^ l).| ) by TAYLOR_2:1;
A4: dom ((a,b) Subnomial n) = dom (Newton_Coeff n) by DOMN
.= dom ((|.a.|,|.b.|) Subnomial n) by DOMN ;
|.((a |^ k) * (b |^ l)).| >= (a |^ k) * (b |^ l) by ABSVALUE:4;
then |.(a |^ k).| * |.(b |^ l).| >= (a |^ k) * (b |^ l) by COMPLEX1:65;
then (|.a.| |^ k) * (|.b.| |^ l) >= ((a,b) Subnomial (l + k)) . (l + 1) by A0, A2, A3, LmS1;
hence ((a,b) Subnomial n) . i <= ((|.a.|,|.b.|) Subnomial n) . i by A0, A2, A4, LmS1; :: thesis: verum

end;

end;