let m, n, b be Nat; :: thesis: ( b > 1 implies ( ( len (digits (m,b)) < len (digits (n,b)) or ( len (digits (m,b)) = len (digits (n,b)) & ex i being Nat st
( i < len (digits (m,b)) & (digits (m,b)) . i < (digits (n,b)) . i & ( for j being Nat st j < len (digits (m,b)) & (digits (m,b)) . j <> (digits (n,b)) . j holds
i >= j ) ) ) ) iff m < n ) )
set dm = digits (m,b);
set dn = digits (n,b);
consider vm being XFinSequence of NAT such that
A1: ( dom vm = dom (digits (m,b)) & ( for i being Nat st i in dom vm holds
vm . i = ((digits (m,b)) . i) * (b |^ i) ) & value ((digits (m,b)),b) = Sum vm ) by NUMERAL1:def 1;
consider vn being XFinSequence of NAT such that
A2: ( dom vn = dom (digits (n,b)) & ( for i being Nat st i in dom vn holds
vn . i = ((digits (n,b)) . i) * (b |^ i) ) & value ((digits (n,b)),b) = Sum vn ) by NUMERAL1:def 1;
assume A3: b > 1 ; :: thesis: ( ( len (digits (m,b)) < len (digits (n,b)) or ( len (digits (m,b)) = len (digits (n,b)) & ex i being Nat st
( i < len (digits (m,b)) & (digits (m,b)) . i < (digits (n,b)) . i & ( for j being Nat st j < len (digits (m,b)) & (digits (m,b)) . j <> (digits (n,b)) . j holds
i >= j ) ) ) ) iff m < n )
thus ( not m < n or len (digits (m,b)) < len (digits (n,b)) or ( len (digits (m,b)) = len (digits (n,b)) & ex i being Nat st
( i < len (digits (m,b)) & (digits (m,b)) . i < (digits (n,b)) . i & ( for j being Nat st j < len (digits (m,b)) & (digits (m,b)) . j <> (digits (n,b)) . j holds
i >= j ) ) ) ) :: thesis: ( ( len (digits (m,b)) < len (digits (n,b)) or ( len (digits (m,b)) = len (digits (n,b)) & ex i being Nat st
( i < len (digits (m,b)) & (digits (m,b)) . i < (digits (n,b)) . i & ( for j being Nat st j < len (digits (m,b)) & (digits (m,b)) . j <> (digits (n,b)) . j holds
i >= j ) ) ) ) implies m < n )

proof

assume A4: m < n ; :: thesis: ( len (digits (m,b)) < len (digits (n,b)) or ( len (digits (m,b)) = len (digits (n,b)) & ex i being Nat st
( i < len (digits (m,b)) & (digits (m,b)) . i < (digits (n,b)) . i & ( for j being Nat st j < len (digits (m,b)) & (digits (m,b)) . j <> (digits (n,b)) . j holds
i >= j ) ) ) )
assume A5: len (digits (m,b)) >= len (digits (n,b)) ; :: thesis: ( len (digits (m,b)) = len (digits (n,b)) & ex i being Nat st
( i < len (digits (m,b)) & (digits (m,b)) . i < (digits (n,b)) . i & ( for j being Nat st j < len (digits (m,b)) & (digits (m,b)) . j <> (digits (n,b)) . j holds
i >= j ) ) )

now :: thesis: not len (digits (m,b)) > len (digits (n,b))

assume A6: len (digits (m,b)) > len (digits (n,b)) ; :: thesis: contradiction

A7: now :: thesis: not m = 0

assume m = 0 ; :: thesis: contradiction
then digits (m,b) = <%0%> by NUMERAL1:def 2, A3;
then len (digits (m,b)) = 1 by AFINSQ_1:def 4;
hence contradiction by A3, A6, NUMERAL1:4; :: thesis: verum

end;

( m >= b |^ (len (digits (n,b))) & n < b |^ (len (digits (n,b))) ) by A6, A3, A7, Th10, Th9;
hence contradiction by A4, XXREAL_0:2; :: thesis: verum

end;

hence A8: len (digits (m,b)) = len (digits (n,b)) by A5, XXREAL_0:1; :: thesis: ex i being Nat st
( i < len (digits (m,b)) & (digits (m,b)) . i < (digits (n,b)) . i & ( for j being Nat st j < len (digits (m,b)) & (digits (m,b)) . j <> (digits (n,b)) . j holds
i >= j ) )
defpred S₁[ Nat] means ( $1 < len (digits (m,b)) & (digits (m,b)) . $1 <> (digits (n,b)) . $1 );
deffunc H₁() -> M3( NAT ) = len (digits (m,b));
A9: for k being Nat st S₁[k] holds
k <= H₁() ;
A10: ex k being Nat st S₁[k]

proof

assume A11: for k being Nat holds not S₁[k] ; :: thesis: contradiction

now :: thesis: for a being object st a in dom (digits (m,b)) holds
(digits (m,b)) . a = (digits (n,b)) . a

let a be object ; :: thesis: ( a in dom (digits (m,b)) implies (digits (m,b)) . a = (digits (n,b)) . a )
assume a in dom (digits (m,b)) ; :: thesis: (digits (m,b)) . a = (digits (n,b)) . a
then A12: a in Segm (dom (digits (m,b))) ;
then reconsider k = a as Nat ;
k < len (digits (m,b)) by A12, NAT_1:44;
hence (digits (m,b)) . a = (digits (n,b)) . a by A11; :: thesis: verum

end;

then digits (m,b) = digits (n,b) by A8, FUNCT_1:2;
then m = value ((digits (n,b)),b) by A3, NUMERAL1:5;
then m = n by A3, NUMERAL1:5;
hence contradiction by A4; :: thesis: verum

end;

consider i being Nat such that
A13: ( S₁[i] & ( for n being Nat st S₁[n] holds
n <= i ) ) from NAT_1:sch 6(A9, A10);
take i ; :: thesis: ( i < len (digits (m,b)) & (digits (m,b)) . i < (digits (n,b)) . i & ( for j being Nat st j < len (digits (m,b)) & (digits (m,b)) . j <> (digits (n,b)) . j holds
i >= j ) )
thus i < len (digits (m,b)) by A13; :: thesis: ( (digits (m,b)) . i < (digits (n,b)) . i & ( for j being Nat st j < len (digits (m,b)) & (digits (m,b)) . j <> (digits (n,b)) . j holds
i >= j ) )
thus (digits (m,b)) . i < (digits (n,b)) . i :: thesis: for j being Nat st j < len (digits (m,b)) & (digits (m,b)) . j <> (digits (n,b)) . j holds
i >= j

proof

assume not (digits (m,b)) . i < (digits (n,b)) . i ; :: thesis: contradiction
then A14: (digits (m,b)) . i > (digits (n,b)) . i by A13, XXREAL_0:1;
A15: ( i in Segm (dom (digits (m,b))) & i in Segm (dom (digits (n,b))) ) by A8, A13, NAT_1:44;

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

suppose A16: i > 0 ; :: thesis: contradiction

A17: now :: thesis: not n = 0

assume n = 0 ; :: thesis: contradiction
then digits (n,b) = <%0%> by A3, NUMERAL1:def 2;
then ( i < 1 & i >= 0 + 1 ) by A13, A8, A16, AFINSQ_1:34, NAT_1:14;
hence contradiction ; :: thesis: verum

end;

vm = (vm | i) ^ (vm /^ i) ;
then A18: Sum vm = (Sum (vm | i)) + (Sum (vm /^ i)) by AFINSQ_2:55;
vn = (vn | i) ^ (vn /^ i) ;
then A19: Sum vn = (Sum (vn | i)) + (Sum (vn /^ i)) by AFINSQ_2:55;
len (digits (m,b)) >= 0 + 1 by A3, NUMERAL1:4;
then reconsider ldm1 = (len (digits (m,b))) - 1 as Nat by NAT_1:20;
i < ldm1 + 1 by A13;
then i <= ldm1 by NAT_1:13;

per cases then ( i = ldm1 or i < ldm1 ) by XXREAL_0:1;

suppose A20: i = ldm1 ; :: thesis: contradiction

then i < len (digits (m,b)) by XREAL_1:44;
then A21: len (vm /^ i) = (len vm) - i by A1, AFINSQ_2:7
.= 1 by A20, A1 ;
then 0 in Segm (dom (vm /^ i)) by NAT_1:44;
then (vm /^ i) . 0 = vm . (0 + i) by AFINSQ_2:def 2;
then vm /^ i = <%(vm . i)%> by A21, AFINSQ_1:34;
then A22: Sum (vm /^ i) = vm . i by AFINSQ_2:53;
i < len (digits (m,b)) by A20, XREAL_1:44;
then A23: len (vn /^ i) = (len vn) - i by A8, A2, AFINSQ_2:7
.= 1 by A8, A20, A2 ;
then 0 in Segm (dom (vn /^ i)) by NAT_1:44;
then (vn /^ i) . 0 = vn . (0 + i) by AFINSQ_2:def 2;
then vn /^ i = <%(vn . i)%> by A23, AFINSQ_1:34;
then A24: Sum (vn /^ i) = vn . i by AFINSQ_2:53;
A25: ( dom ((digits (n,b)) | i) c= dom (digits (n,b)) & dom (vn | i) c= dom vn ) by RELAT_1:60;
consider d9 being XFinSequence of NAT such that
A26: ( dom d9 = dom ((digits (n,b)) | i) & ( for a being Nat st a in dom d9 holds
d9 . a = (((digits (n,b)) | i) . a) * (b |^ a) ) & value (((digits (n,b)) | i),b) = Sum d9 ) by NUMERAL1:def 1;
A27: dom d9 = i by A26, A8, A13, AFINSQ_1:54
.= dom (vn | i) by A2, A8, A13, AFINSQ_1:54 ;

now :: thesis: for a being Nat st a in dom d9 holds
d9 . a = (vn | i) . a

let a be Nat; :: thesis: ( a in dom d9 implies d9 . a = (vn | i) . a )
assume A28: a in dom d9 ; :: thesis: d9 . a = (vn | i) . a
then d9 . a = (((digits (n,b)) | i) . a) * (b |^ a) by A26;
then A29: d9 . a = ((digits (n,b)) . a) * (b |^ a) by A28, A26, FUNCT_1:47;
A30: a in dom (vn | i) by A28, A27;
then A31: (vn | i) . a = vn . a by FUNCT_1:47;
a in dom vn by A30, A25;
then (vn | i) . a = ((digits (n,b)) . a) * (b |^ a) by A31, A2;
hence d9 . a = (vn | i) . a by A29; :: thesis: verum

end;

then d9 = vn | i by A27, AFINSQ_1:8;
then A32: value (((digits (n,b)) | i),b) = Sum (vn | i) by A26;
A33: len ((digits (n,b)) | i) > 0 by A8, A13, A16, AFINSQ_1:54;
for a being Nat st a in dom ((digits (n,b)) | i) holds
((digits (n,b)) | i) . a < b

proof

let a be Nat; :: thesis: ( a in dom ((digits (n,b)) | i) implies ((digits (n,b)) | i) . a < b )
assume a in dom ((digits (n,b)) | i) ; :: thesis: ((digits (n,b)) | i) . a < b
then ( a in dom (digits (n,b)) & ((digits (n,b)) | i) . a = (digits (n,b)) . a ) by A25, FUNCT_1:47;
hence ((digits (n,b)) | i) . a < b by A17, NUMERAL1:def 2, A3; :: thesis: verum

end;

then value (((digits (n,b)) | i),b) < b |^ (len ((digits (n,b)) | i)) by A33, Th8, A3;
then value (((digits (n,b)) | i),b) < b |^ i by A8, A13, AFINSQ_1:54;
then Sum (vn | i) < b |^ i by A32;
then (Sum (vn | i)) + (vn . i) < (b |^ i) + (vn . i) by XREAL_1:6;
then (Sum (vn | i)) + (vn . i) < (b |^ i) + (((digits (n,b)) . i) * (b |^ i)) by A2, A15;
then A34: (Sum (vn | i)) + (vn . i) < (b |^ i) * (1 + ((digits (n,b)) . i)) ;
1 + ((digits (n,b)) . i) <= (digits (m,b)) . i by A14, NAT_1:13;
then (b |^ i) * (1 + ((digits (n,b)) . i)) <= (b |^ i) * ((digits (m,b)) . i) by XREAL_1:64;
then (b |^ i) * (1 + ((digits (n,b)) . i)) <= vm . i by A15, A1;
then (Sum (vn | i)) + (vn . i) < vm . i by A34, XXREAL_0:2;
then (Sum (vn | i)) + (Sum (vn /^ i)) < Sum (vm /^ i) by A22, A24;
then (Sum (vn | i)) + (Sum (vn /^ i)) < (Sum (vm | i)) + (Sum (vm /^ i)) by XREAL_1:40;
then Sum vn < Sum vm by A18, A19;
then n < Sum vm by A2, A3, NUMERAL1:5;
hence contradiction by A4, A1, A3, NUMERAL1:5; :: thesis: verum

end;

suppose A35: i < ldm1 ; :: thesis: contradiction

( i < (len (digits (m,b))) - 1 & (len (digits (m,b))) - 1 < len (digits (m,b)) ) by A35, XREAL_1:44;
then i < len (digits (m,b)) by XXREAL_0:2;
then A36: len (vm /^ i) = (len vm) - i by A1, AFINSQ_2:7;
A37: len (vm /^ i) > 0 by A36, A13, A1, XREAL_1:50;
then reconsider vmi = vm /^ i as non empty XFinSequence of NAT ;
0 in Segm (dom (vm /^ i)) by A37, NAT_1:44;
then A38: vmi . 0 = vm . (0 + i) by AFINSQ_2:def 2;
A39: vmi = <%(vmi . 0)%> ^ (vmi /^ 1) by NUMERAL2:2;
set c = Sum (vmi /^ 1);
A40: Sum (vm /^ i) = (Sum <%(vmi . 0)%>) + (Sum (vmi /^ 1)) by A39, AFINSQ_2:55
.= (vm . i) + (Sum (vmi /^ 1)) by A38, AFINSQ_2:53 ;
( i < (len (digits (n,b))) - 1 & (len (digits (n,b))) - 1 < len (digits (n,b)) ) by A8, A35, XREAL_1:44;
then i < len (digits (n,b)) by XXREAL_0:2;
then A41: len (vn /^ i) = (len vn) - i by A2, AFINSQ_2:7;
A42: len (vn /^ i) > 0 by A8, A41, A13, A2, XREAL_1:50;
then reconsider vni = vn /^ i as non empty XFinSequence of NAT ;
0 in Segm (dom (vn /^ i)) by A42, NAT_1:44;
then A43: vni . 0 = vn . (0 + i) by AFINSQ_2:def 2;
A44: vni = <%(vni . 0)%> ^ (vni /^ 1) by NUMERAL2:2;
set d = Sum (vni /^ 1);
A45: Sum (vn /^ i) = (Sum <%(vni . 0)%>) + (Sum (vni /^ 1)) by A44, AFINSQ_2:55
.= (vn . i) + (Sum (vni /^ 1)) by A43, AFINSQ_2:53 ;
A46: len (vni /^ 1) = (len vmi) -' 1 by A41, A36, A2, A1, A8, AFINSQ_2:def 2;

now :: thesis: for a being Nat st a in dom (vni /^ 1) holds
(vni /^ 1) . a = vmi . (a + 1)

let a be Nat; :: thesis: ( a in dom (vni /^ 1) implies (vni /^ 1) . a = vmi . (a + 1) )
assume A47: a in dom (vni /^ 1) ; :: thesis: (vni /^ 1) . a = vmi . (a + 1)
i <= (len vn) - 1 by A35, A2, A8;
then (len vn) - i >= 1 by XREAL_1:11;
then A48: len vni >= 1 by A41;
len (vni /^ 1) = (len vni) -' 1 by AFINSQ_2:def 2;
then len (vni /^ 1) = Segm ((len vni) - 1) by XREAL_1:233, A48;
then a < (len vni) - 1 by NAT_1:44, A47;
then A49: a + 1 < ((len vni) - 1) + 1 by XREAL_1:6;
then A50: a + 1 in Segm (dom vni) by NAT_1:44;
a + 1 < (len vn) - i by A41, A49;
then A51: i + (a + 1) < ((len vn) - i) + i by XREAL_1:6;
then A52: i + (a + 1) in Segm (dom vn) by NAT_1:44;
i + (a + 1) > i by XREAL_1:29;
then A53: (digits (n,b)) . (i + (a + 1)) = (digits (m,b)) . (i + (a + 1)) by A13, A51, A2, A8;
thus (vni /^ 1) . a = vni . (a + 1) by A47, AFINSQ_2:def 2
.= vn . (i + (a + 1)) by A50, AFINSQ_2:def 2
.= ((digits (m,b)) . (i + (a + 1))) * (b |^ (i + (a + 1))) by A53, A52, A2
.= vm . (i + (a + 1)) by A52, A1, A2, A8
.= vmi . (a + 1) by A36, A41, A8, A2, A1, A50, AFINSQ_2:def 2 ; :: thesis: verum

end;

then A54: vmi /^ 1 = vni /^ 1 by A46, AFINSQ_2:def 2;
A55: ( dom ((digits (n,b)) | i) c= dom (digits (n,b)) & dom (vn | i) c= dom vn ) by RELAT_1:60;
consider d9 being XFinSequence of NAT such that
A56: ( dom d9 = dom ((digits (n,b)) | i) & ( for a being Nat st a in dom d9 holds
d9 . a = (((digits (n,b)) | i) . a) * (b |^ a) ) & value (((digits (n,b)) | i),b) = Sum d9 ) by NUMERAL1:def 1;
A57: dom d9 = i by A8, A56, A13, AFINSQ_1:54
.= dom (vn | i) by A8, A2, A13, AFINSQ_1:54 ;

now :: thesis: for a being Nat st a in dom d9 holds
d9 . a = (vn | i) . a

let a be Nat; :: thesis: ( a in dom d9 implies d9 . a = (vn | i) . a )
assume A58: a in dom d9 ; :: thesis: d9 . a = (vn | i) . a
then d9 . a = (((digits (n,b)) | i) . a) * (b |^ a) by A56;
then A59: d9 . a = ((digits (n,b)) . a) * (b |^ a) by A58, A56, FUNCT_1:47;
A60: a in dom (vn | i) by A58, A57;
then A61: (vn | i) . a = vn . a by FUNCT_1:47;
a in dom vn by A60, A55;
then (vn | i) . a = ((digits (n,b)) . a) * (b |^ a) by A61, A2;
hence d9 . a = (vn | i) . a by A59; :: thesis: verum

end;

then d9 = vn | i by A57, AFINSQ_1:8;
then A62: value (((digits (n,b)) | i),b) = Sum (vn | i) by A56;
A63: len ((digits (n,b)) | i) > 0 by A8, A13, A16, AFINSQ_1:54;
for a being Nat st a in dom ((digits (n,b)) | i) holds
((digits (n,b)) | i) . a < b

proof

let a be Nat; :: thesis: ( a in dom ((digits (n,b)) | i) implies ((digits (n,b)) | i) . a < b )
assume a in dom ((digits (n,b)) | i) ; :: thesis: ((digits (n,b)) | i) . a < b
then ( a in dom (digits (n,b)) & ((digits (n,b)) | i) . a = (digits (n,b)) . a ) by A55, FUNCT_1:47;
hence ((digits (n,b)) | i) . a < b by A17, NUMERAL1:def 2, A3; :: thesis: verum

end;

then value (((digits (n,b)) | i),b) < b |^ (len ((digits (n,b)) | i)) by A63, Th8, A3;
then value (((digits (n,b)) | i),b) < b |^ i by A13, A8, AFINSQ_1:54;
then Sum (vn | i) < b |^ i by A62;
then (Sum (vn | i)) + (vn . i) < (b |^ i) + (vn . i) by XREAL_1:6;
then (Sum (vn | i)) + (vn . i) < (b |^ i) + (((digits (n,b)) . i) * (b |^ i)) by A2, A15;
then A64: (Sum (vn | i)) + (vn . i) < (b |^ i) * (1 + ((digits (n,b)) . i)) ;
1 + ((digits (n,b)) . i) <= (digits (m,b)) . i by A14, NAT_1:13;
then (b |^ i) * (1 + ((digits (n,b)) . i)) <= (b |^ i) * ((digits (m,b)) . i) by XREAL_1:64;
then (b |^ i) * (1 + ((digits (n,b)) . i)) <= vm . i by A15, A1;
then (Sum (vn | i)) + (vn . i) < vm . i by A64, XXREAL_0:2;
then ((Sum (vn | i)) + (vn . i)) + (Sum (vmi /^ 1)) < (vm . i) + (Sum (vmi /^ 1)) by XREAL_1:6;
then (Sum (vn | i)) + (Sum (vn /^ i)) < Sum (vm /^ i) by A54, A40, A45;
then (Sum (vn | i)) + (Sum (vn /^ i)) < (Sum (vm | i)) + (Sum (vm /^ i)) by XREAL_1:40;
then Sum vn < Sum vm by A18, A19;
then n < Sum vm by A2, A3, NUMERAL1:5;
hence contradiction by A4, A1, A3, NUMERAL1:5; :: thesis: verum

end;

end;

end;

suppose A65: i = 0 ; :: thesis: contradiction

A66: len ((digits (n,b)) /^ 1) = (len (digits (m,b))) -' 1 by A8, AFINSQ_2:def 2;
for a being Nat st a in dom ((digits (n,b)) /^ 1) holds
((digits (n,b)) /^ 1) . a = (digits (m,b)) . (a + 1)

proof

let a be Nat; :: thesis: ( a in dom ((digits (n,b)) /^ 1) implies ((digits (n,b)) /^ 1) . a = (digits (m,b)) . (a + 1) )
assume A67: a in dom ((digits (n,b)) /^ 1) ; :: thesis: ((digits (n,b)) /^ 1) . a = (digits (m,b)) . (a + 1)
len (digits (m,b)) >= 1 by A3, NUMERAL1:4;
then A68: (len (digits (m,b))) -' 1 = (len (digits (m,b))) - 1 by XREAL_1:233;
a < Segm (len ((digits (n,b)) /^ 1)) by A67, NAT_1:44;
then A69: ( a + 1 < ((len (digits (m,b))) - 1) + 1 & a + 1 > i ) by A66, A68, A65, XREAL_1:6;
thus ((digits (n,b)) /^ 1) . a = (digits (n,b)) . (a + 1) by A67, AFINSQ_2:def 2
.= (digits (m,b)) . (a + 1) by A69, A13 ; :: thesis: verum

end;

then A70: (digits (m,b)) /^ 1 = (digits (n,b)) /^ 1 by A66, AFINSQ_2:def 2;
mid ((digits (n,b)),2,(len (digits (n,b)))) = (digits (m,b)) /^ 1 by A70, NUMERAL2:3
.= mid ((digits (m,b)),2,(len (digits (m,b)))) by NUMERAL2:3 ;
then (b * (value ((mid ((digits (m,b)),2,(len (digits (m,b))))),b))) + ((digits (m,b)) . i) > (b * (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b))) + ((digits (n,b)) . i) by A14, XREAL_1:8;
then m > (b * (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b))) + ((digits (n,b)) . i) by A65, A3, NUMERAL2:19;
hence contradiction by A4, A65, A3, NUMERAL2:19; :: thesis: verum

end;

end;

end;

thus for j being Nat st j < len (digits (m,b)) & (digits (m,b)) . j <> (digits (n,b)) . j holds
i >= j by A13; :: thesis: verum

end;

thus ( ( len (digits (m,b)) < len (digits (n,b)) or ( len (digits (m,b)) = len (digits (n,b)) & ex i being Nat st
( i < len (digits (m,b)) & (digits (m,b)) . i < (digits (n,b)) . i & ( for j being Nat st j < len (digits (m,b)) & (digits (m,b)) . j <> (digits (n,b)) . j holds
i >= j ) ) ) ) implies m < n ) :: thesis: verum

proof

assume ( len (digits (m,b)) < len (digits (n,b)) or ( len (digits (m,b)) = len (digits (n,b)) & ex i being Nat st
( i < len (digits (m,b)) & (digits (m,b)) . i < (digits (n,b)) . i & ( for j being Nat st j < len (digits (m,b)) & (digits (m,b)) . j <> (digits (n,b)) . j holds
i >= j ) ) ) ) ; :: thesis: m < n

per cases then ( len (digits (m,b)) < len (digits (n,b)) or ( len (digits (m,b)) = len (digits (n,b)) & ex i being Nat st
( i < len (digits (m,b)) & (digits (m,b)) . i < (digits (n,b)) . i & ( for j being Nat st j < len (digits (m,b)) & (digits (m,b)) . j <> (digits (n,b)) . j holds
i >= j ) ) ) ) ;

suppose A71: len (digits (m,b)) < len (digits (n,b)) ; :: thesis: m < n

1 <= len (digits (m,b)) by NUMERAL1:4, A3;
then A72: len (digits (n,b)) > 1 by A71, XXREAL_0:2;
len (digits (0,b)) = len <%0%> by NUMERAL1:def 2, A3;
then A73: n <> 0 by A72, AFINSQ_1:34;
( m < b |^ (len (digits (m,b))) & b |^ (len (digits (m,b))) <= n ) by A3, A71, Th9, Th10, A73;
hence m < n by XXREAL_0:2; :: thesis: verum

end;

suppose A74: ( len (digits (m,b)) = len (digits (n,b)) & ex i being Nat st
( i < len (digits (m,b)) & (digits (m,b)) . i < (digits (n,b)) . i & ( for j being Nat st j < len (digits (m,b)) & (digits (m,b)) . j <> (digits (n,b)) . j holds
i >= j ) ) ) ; :: thesis: m < n

then consider i being Nat such that
A75: ( i < len (digits (m,b)) & (digits (m,b)) . i < (digits (n,b)) . i & ( for j being Nat st j < len (digits (m,b)) & (digits (m,b)) . j <> (digits (n,b)) . j holds
i >= j ) ) ;
A76: ( i in Segm (dom (digits (m,b))) & i in Segm (dom (digits (n,b))) ) by A74, A75, NAT_1:44;

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

suppose A77: i > 0 ; :: thesis: m < n

A78: now :: thesis: not m = 0

assume m = 0 ; :: thesis: contradiction
then digits (m,b) = <%0%> by A3, NUMERAL1:def 2;
then ( i < 1 & i >= 0 + 1 ) by A75, A77, AFINSQ_1:34, NAT_1:14;
hence contradiction ; :: thesis: verum

end;

vm = (vm | i) ^ (vm /^ i) ;
then A79: Sum vm = (Sum (vm | i)) + (Sum (vm /^ i)) by AFINSQ_2:55;
vn = (vn | i) ^ (vn /^ i) ;
then A80: Sum vn = (Sum (vn | i)) + (Sum (vn /^ i)) by AFINSQ_2:55;
len (digits (m,b)) >= 0 + 1 by A3, NUMERAL1:4;
then reconsider ldm1 = (len (digits (m,b))) - 1 as Nat by NAT_1:20;
i < ldm1 + 1 by A75;
then i <= ldm1 by NAT_1:13;

per cases then ( i = ldm1 or i < ldm1 ) by XXREAL_0:1;

suppose A81: i = ldm1 ; :: thesis: m < n

then i < len (digits (m,b)) by XREAL_1:44;
then A82: len (vm /^ i) = (len vm) - i by A1, AFINSQ_2:7
.= 1 by A81, A1 ;
then 0 in Segm (dom (vm /^ i)) by NAT_1:44;
then (vm /^ i) . 0 = vm . (0 + i) by AFINSQ_2:def 2;
then vm /^ i = <%(vm . i)%> by A82, AFINSQ_1:34;
then A83: Sum (vm /^ i) = vm . i by AFINSQ_2:53;
i < len (digits (m,b)) by A81, XREAL_1:44;
then A84: len (vn /^ i) = (len vn) - i by A74, A2, AFINSQ_2:7
.= 1 by A74, A81, A2 ;
then 0 in Segm (dom (vn /^ i)) by NAT_1:44;
then (vn /^ i) . 0 = vn . (0 + i) by AFINSQ_2:def 2;
then vn /^ i = <%(vn . i)%> by A84, AFINSQ_1:34;
then A85: Sum (vn /^ i) = vn . i by AFINSQ_2:53;
A86: ( dom ((digits (m,b)) | i) c= dom (digits (m,b)) & dom (vm | i) c= dom vm ) by RELAT_1:60;
consider d9 being XFinSequence of NAT such that
A87: ( dom d9 = dom ((digits (m,b)) | i) & ( for a being Nat st a in dom d9 holds
d9 . a = (((digits (m,b)) | i) . a) * (b |^ a) ) & value (((digits (m,b)) | i),b) = Sum d9 ) by NUMERAL1:def 1;
A88: dom d9 = i by A87, A75, AFINSQ_1:54
.= dom (vm | i) by A1, A75, AFINSQ_1:54 ;

now :: thesis: for a being Nat st a in dom d9 holds
d9 . a = (vm | i) . a

let a be Nat; :: thesis: ( a in dom d9 implies d9 . a = (vm | i) . a )
assume A89: a in dom d9 ; :: thesis: d9 . a = (vm | i) . a
then d9 . a = (((digits (m,b)) | i) . a) * (b |^ a) by A87;
then A90: d9 . a = ((digits (m,b)) . a) * (b |^ a) by A89, A87, FUNCT_1:47;
A91: a in dom (vm | i) by A89, A88;
then A92: (vm | i) . a = vm . a by FUNCT_1:47;
a in dom vm by A91, A86;
then (vm | i) . a = ((digits (m,b)) . a) * (b |^ a) by A92, A1;
hence d9 . a = (vm | i) . a by A90; :: thesis: verum

end;

then d9 = vm | i by A88, AFINSQ_1:8;
then A93: value (((digits (m,b)) | i),b) = Sum (vm | i) by A87;
A94: len ((digits (m,b)) | i) > 0 by A75, A77, AFINSQ_1:54;
for a being Nat st a in dom ((digits (m,b)) | i) holds
((digits (m,b)) | i) . a < b

proof

let a be Nat; :: thesis: ( a in dom ((digits (m,b)) | i) implies ((digits (m,b)) | i) . a < b )
assume a in dom ((digits (m,b)) | i) ; :: thesis: ((digits (m,b)) | i) . a < b
then ( a in dom (digits (m,b)) & ((digits (m,b)) | i) . a = (digits (m,b)) . a ) by A86, FUNCT_1:47;
hence ((digits (m,b)) | i) . a < b by A78, NUMERAL1:def 2, A3; :: thesis: verum

end;

then value (((digits (m,b)) | i),b) < b |^ (len ((digits (m,b)) | i)) by A94, Th8, A3;
then value (((digits (m,b)) | i),b) < b |^ i by A75, AFINSQ_1:54;
then Sum (vm | i) < b |^ i by A93;
then (Sum (vm | i)) + (vm . i) < (b |^ i) + (vm . i) by XREAL_1:6;
then (Sum (vm | i)) + (vm . i) < (b |^ i) + (((digits (m,b)) . i) * (b |^ i)) by A1, A76;
then A95: (Sum (vm | i)) + (vm . i) < (b |^ i) * (1 + ((digits (m,b)) . i)) ;
1 + ((digits (m,b)) . i) <= (digits (n,b)) . i by A75, NAT_1:13;
then (b |^ i) * (1 + ((digits (m,b)) . i)) <= (b |^ i) * ((digits (n,b)) . i) by XREAL_1:64;
then (b |^ i) * (1 + ((digits (m,b)) . i)) <= vn . i by A76, A2;
then (Sum (vm | i)) + (vm . i) < vn . i by A95, XXREAL_0:2;
then (Sum (vm | i)) + (Sum (vm /^ i)) < Sum (vn /^ i) by A83, A85;
then (Sum (vm | i)) + (Sum (vm /^ i)) < (Sum (vn | i)) + (Sum (vn /^ i)) by XREAL_1:40;
then Sum vm < Sum vn by A79, A80;
then m < Sum vn by A1, A3, NUMERAL1:5;
hence m < n by A2, A3, NUMERAL1:5; :: thesis: verum

end;

suppose A96: i < ldm1 ; :: thesis: m < n

( i < (len (digits (m,b))) - 1 & (len (digits (m,b))) - 1 < len (digits (m,b)) ) by A96, XREAL_1:44;
then i < len (digits (m,b)) by XXREAL_0:2;
then A97: len (vm /^ i) = (len vm) - i by A1, AFINSQ_2:7;
A98: len (vm /^ i) > 0 by A97, A75, A1, XREAL_1:50;
then reconsider vmi = vm /^ i as non empty XFinSequence of NAT ;
0 in Segm (dom (vm /^ i)) by A98, NAT_1:44;
then A99: vmi . 0 = vm . (0 + i) by AFINSQ_2:def 2;
A100: vmi = <%(vmi . 0)%> ^ (vmi /^ 1) by NUMERAL2:2;
set c = Sum (vmi /^ 1);
A101: Sum (vm /^ i) = (Sum <%(vmi . 0)%>) + (Sum (vmi /^ 1)) by A100, AFINSQ_2:55
.= (vm . i) + (Sum (vmi /^ 1)) by A99, AFINSQ_2:53 ;
( i < (len (digits (n,b))) - 1 & (len (digits (n,b))) - 1 < len (digits (n,b)) ) by A74, A96, XREAL_1:44;
then i < len (digits (n,b)) by XXREAL_0:2;
then A102: len (vn /^ i) = (len vn) - i by A2, AFINSQ_2:7;
A103: len (vn /^ i) > 0 by A74, A102, A75, A2, XREAL_1:50;
then reconsider vni = vn /^ i as non empty XFinSequence of NAT ;
0 in Segm (dom (vn /^ i)) by A103, NAT_1:44;
then A104: vni . 0 = vn . (0 + i) by AFINSQ_2:def 2;
A105: vni = <%(vni . 0)%> ^ (vni /^ 1) by NUMERAL2:2;
set d = Sum (vni /^ 1);
A106: Sum (vn /^ i) = (Sum <%(vni . 0)%>) + (Sum (vni /^ 1)) by A105, AFINSQ_2:55
.= (vn . i) + (Sum (vni /^ 1)) by A104, AFINSQ_2:53 ;
A107: len (vni /^ 1) = (len vmi) -' 1 by A102, A97, A2, A1, A74, AFINSQ_2:def 2;

now :: thesis: for a being Nat st a in dom (vni /^ 1) holds
(vni /^ 1) . a = vmi . (a + 1)

let a be Nat; :: thesis: ( a in dom (vni /^ 1) implies (vni /^ 1) . a = vmi . (a + 1) )
assume A108: a in dom (vni /^ 1) ; :: thesis: (vni /^ 1) . a = vmi . (a + 1)
i <= (len vn) - 1 by A96, A2, A74;
then (len vn) - i >= 1 by XREAL_1:11;
then A109: len vni >= 1 by A102;
len (vni /^ 1) = (len vni) -' 1 by AFINSQ_2:def 2;
then len (vni /^ 1) = Segm ((len vni) - 1) by XREAL_1:233, A109;
then a < (len vni) - 1 by NAT_1:44, A108;
then A110: a + 1 < ((len vni) - 1) + 1 by XREAL_1:6;
then A111: a + 1 in Segm (dom vni) by NAT_1:44;
a + 1 < (len vn) - i by A102, A110;
then A112: i + (a + 1) < ((len vn) - i) + i by XREAL_1:6;
then A113: i + (a + 1) in Segm (dom vn) by NAT_1:44;
i + (a + 1) > i by XREAL_1:29;
then A114: (digits (n,b)) . (i + (a + 1)) = (digits (m,b)) . (i + (a + 1)) by A75, A112, A2, A74;
thus (vni /^ 1) . a = vni . (a + 1) by A108, AFINSQ_2:def 2
.= vn . (i + (a + 1)) by A111, AFINSQ_2:def 2
.= ((digits (m,b)) . (i + (a + 1))) * (b |^ (i + (a + 1))) by A114, A113, A2
.= vm . (i + (a + 1)) by A113, A1, A2, A74
.= vmi . (a + 1) by A97, A102, A74, A2, A1, A111, AFINSQ_2:def 2 ; :: thesis: verum

end;

then A115: vmi /^ 1 = vni /^ 1 by A107, AFINSQ_2:def 2;
A116: ( dom ((digits (m,b)) | i) c= dom (digits (m,b)) & dom (vm | i) c= dom vm ) by RELAT_1:60;
consider d9 being XFinSequence of NAT such that
A117: ( dom d9 = dom ((digits (m,b)) | i) & ( for a being Nat st a in dom d9 holds
d9 . a = (((digits (m,b)) | i) . a) * (b |^ a) ) & value (((digits (m,b)) | i),b) = Sum d9 ) by NUMERAL1:def 1;
A118: dom d9 = i by A117, A75, AFINSQ_1:54
.= dom (vm | i) by A1, A75, AFINSQ_1:54 ;

now :: thesis: for a being Nat st a in dom d9 holds
d9 . a = (vm | i) . a

let a be Nat; :: thesis: ( a in dom d9 implies d9 . a = (vm | i) . a )
assume A119: a in dom d9 ; :: thesis: d9 . a = (vm | i) . a
then d9 . a = (((digits (m,b)) | i) . a) * (b |^ a) by A117;
then A120: d9 . a = ((digits (m,b)) . a) * (b |^ a) by A119, A117, FUNCT_1:47;
A121: a in dom (vm | i) by A119, A118;
then A122: (vm | i) . a = vm . a by FUNCT_1:47;
a in dom vm by A121, A116;
then (vm | i) . a = ((digits (m,b)) . a) * (b |^ a) by A122, A1;
hence d9 . a = (vm | i) . a by A120; :: thesis: verum

end;

then d9 = vm | i by A118, AFINSQ_1:8;
then A123: value (((digits (m,b)) | i),b) = Sum (vm | i) by A117;
A124: len ((digits (m,b)) | i) > 0 by A75, A77, AFINSQ_1:54;
for a being Nat st a in dom ((digits (m,b)) | i) holds
((digits (m,b)) | i) . a < b

proof

let a be Nat; :: thesis: ( a in dom ((digits (m,b)) | i) implies ((digits (m,b)) | i) . a < b )
assume a in dom ((digits (m,b)) | i) ; :: thesis: ((digits (m,b)) | i) . a < b
then ( a in dom (digits (m,b)) & ((digits (m,b)) | i) . a = (digits (m,b)) . a ) by A116, FUNCT_1:47;
hence ((digits (m,b)) | i) . a < b by A78, NUMERAL1:def 2, A3; :: thesis: verum

end;

then value (((digits (m,b)) | i),b) < b |^ (len ((digits (m,b)) | i)) by A124, Th8, A3;
then value (((digits (m,b)) | i),b) < b |^ i by A75, AFINSQ_1:54;
then Sum (vm | i) < b |^ i by A123;
then (Sum (vm | i)) + (vm . i) < (b |^ i) + (vm . i) by XREAL_1:6;
then (Sum (vm | i)) + (vm . i) < (b |^ i) + (((digits (m,b)) . i) * (b |^ i)) by A1, A76;
then A125: (Sum (vm | i)) + (vm . i) < (b |^ i) * (1 + ((digits (m,b)) . i)) ;
1 + ((digits (m,b)) . i) <= (digits (n,b)) . i by A75, NAT_1:13;
then (b |^ i) * (1 + ((digits (m,b)) . i)) <= (b |^ i) * ((digits (n,b)) . i) by XREAL_1:64;
then (b |^ i) * (1 + ((digits (m,b)) . i)) <= vn . i by A76, A2;
then (Sum (vm | i)) + (vm . i) < vn . i by A125, XXREAL_0:2;
then ((Sum (vm | i)) + (vm . i)) + (Sum (vmi /^ 1)) < (vn . i) + (Sum (vmi /^ 1)) by XREAL_1:6;
then (Sum (vm | i)) + (Sum (vm /^ i)) < Sum (vn /^ i) by A115, A101, A106;
then (Sum (vm | i)) + (Sum (vm /^ i)) < (Sum (vn | i)) + (Sum (vn /^ i)) by XREAL_1:40;
then Sum vm < Sum vn by A79, A80;
then m < Sum vn by A1, A3, NUMERAL1:5;
hence m < n by A2, A3, NUMERAL1:5; :: thesis: verum

end;

end;

end;

suppose A126: i = 0 ; :: thesis: m < n

A127: len ((digits (n,b)) /^ 1) = (len (digits (m,b))) -' 1 by A74, AFINSQ_2:def 2;
for a being Nat st a in dom ((digits (n,b)) /^ 1) holds
((digits (n,b)) /^ 1) . a = (digits (m,b)) . (a + 1)

proof

let a be Nat; :: thesis: ( a in dom ((digits (n,b)) /^ 1) implies ((digits (n,b)) /^ 1) . a = (digits (m,b)) . (a + 1) )
assume A128: a in dom ((digits (n,b)) /^ 1) ; :: thesis: ((digits (n,b)) /^ 1) . a = (digits (m,b)) . (a + 1)
len (digits (m,b)) >= 1 by A3, NUMERAL1:4;
then A129: (len (digits (m,b))) -' 1 = (len (digits (m,b))) - 1 by XREAL_1:233;
a < Segm (len ((digits (n,b)) /^ 1)) by A128, NAT_1:44;
then A130: ( a + 1 < ((len (digits (m,b))) - 1) + 1 & a + 1 > i ) by A127, A129, A126, XREAL_1:6;
thus ((digits (n,b)) /^ 1) . a = (digits (n,b)) . (a + 1) by A128, AFINSQ_2:def 2
.= (digits (m,b)) . (a + 1) by A130, A75 ; :: thesis: verum

end;

then A131: (digits (m,b)) /^ 1 = (digits (n,b)) /^ 1 by A127, AFINSQ_2:def 2;
mid ((digits (m,b)),2,(len (digits (m,b)))) = (digits (n,b)) /^ 1 by A131, NUMERAL2:3
.= mid ((digits (n,b)),2,(len (digits (n,b)))) by NUMERAL2:3 ;
then (b * (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b))) + ((digits (n,b)) . i) > (b * (value ((mid ((digits (m,b)),2,(len (digits (m,b))))),b))) + ((digits (m,b)) . i) by A75, XREAL_1:8;
then n > (b * (value ((mid ((digits (m,b)),2,(len (digits (m,b))))),b))) + ((digits (m,b)) . i) by A126, A3, NUMERAL2:19;
hence m < n by A126, A3, NUMERAL2:19; :: thesis: verum

end;

end;

end;

end;

end;