let d1, d2 be XFinSequence of NAT ; :: thesis: for b being Nat st b > 1 & dom d1 = dom d2 & ( for n being Nat st n in dom d1 holds
d1 . n <= d2 . n ) holds
value (d1,b) <= value (d2,b)
let b be Nat; :: thesis: ( b > 1 & dom d1 = dom d2 & ( for n being Nat st n in dom d1 holds
d1 . n <= d2 . n ) implies value (d1,b) <= value (d2,b) )
assume A1: ( b > 1 & dom d1 = dom d2 & ( for n being Nat st n in dom d1 holds
d1 . n <= d2 . n ) ) ; :: thesis: value (d1,b) <= value (d2,b)
consider e1 being XFinSequence of NAT such that
A2: ( dom e1 = dom d1 & ( for i being Nat st i in dom e1 holds
e1 . i = (d1 . i) * (b |^ i) ) & value (d1,b) = Sum e1 ) by NUMERAL1:def 1;
consider e2 being XFinSequence of NAT such that
A3: ( dom e2 = dom d2 & ( for i being Nat st i in dom e2 holds
e2 . i = (d2 . i) * (b |^ i) ) & value (d2,b) = Sum e2 ) by NUMERAL1:def 1;

now :: thesis: for i being Nat st i in dom e1 holds
e1 . i <= e2 . i

let i be Nat; :: thesis: ( i in dom e1 implies e1 . i <= e2 . i )
assume A4: i in dom e1 ; :: thesis: e1 . i <= e2 . i
then d1 . i <= d2 . i by A1, A2;
then (d1 . i) * (b |^ i) <= (d2 . i) * (b |^ i) by XREAL_1:64;
then e1 . i <= (d2 . i) * (b |^ i) by A4, A2;
hence e1 . i <= e2 . i by A1, A2, A3, A4; :: thesis: verum

end;

then Sum e1 <= Sum e2 by A1, A2, A3, AFINSQ_2:57;
hence value (d1,b) <= value (d2,b) by A2, A3; :: thesis: verum