set d = (<%0,0%> ^ (11 --> 9)) ^ <%1%>;
A1: len ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) = (len (<%0,0%> ^ (11 --> 9))) + (len <%1%>) by AFINSQ_1:17
.= (len (<%0,0%> ^ (11 --> 9))) + 1 by AFINSQ_1:34 ;
then A2: ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . ((len ((<%0,0%> ^ (11 --> 9)) ^ <%1%>)) - 1) = ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . (len (<%0,0%> ^ (11 --> 9))) ;
then A3: ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . ((len ((<%0,0%> ^ (11 --> 9)) ^ <%1%>)) - 1) > 0 by AFINSQ_1:36;

A4: now :: thesis: for i being Nat st i in dom ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) holds
((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . i < 10

let i be Nat; :: thesis: ( i in dom ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) implies ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . i < 10 )
assume i in dom ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) ; :: thesis: ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . i < 10
then ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . i in rng ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) by FUNCT_1:3;
then ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . i in (rng (<%0,0%> ^ (11 --> 9))) \/ (rng <%1%>) by AFINSQ_1:26;
then ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . i in ((rng <%0,0%>) \/ (rng (11 --> 9))) \/ (rng <%1%>) by AFINSQ_1:26;
then ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . i in ((rng <%0,0%>) \/ (rng (11 --> 9))) \/ {1} by AFINSQ_1:33;
then ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . i in ({0,0} \/ (rng (11 --> 9))) \/ {1} by AFINSQ_1:98;
then ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . i in ({0,0} \/ {9}) \/ {1} by FUNCOP_1:8;
then ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . i in ({0} \/ {9}) \/ {1} by ENUMSET1:29;
then ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . i in {0,9} \/ {1} by ENUMSET1:1;
then ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . i in {0,9,1} by ENUMSET1:3;
then ( ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . i = 0 or ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . i = 9 or ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . i = 1 ) by ENUMSET1:def 1;
hence ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . i < 10 ; :: thesis: verum

end;

A5: digits ((value (((<%0,0%> ^ (11 --> 9)) ^ <%1%>),10)),10) = (<%0,0%> ^ (11 --> 9)) ^ <%1%> by Th5, A3, A4;
thus Sum (digits ((value (((<%0,0%> ^ (11 --> 9)) ^ <%1%>),10)),10)) = (Sum (<%0,0%> ^ (11 --> 9))) + (Sum <%1%>) by AFINSQ_2:55, A5
.= (Sum (<%0,0%> ^ (11 --> 9))) + 1 by AFINSQ_2:53
.= ((Sum <%0,0%>) + (Sum (11 --> 9))) + 1 by AFINSQ_2:55
.= ((0 + 0) + (Sum (11 --> 9))) + 1 by AFINSQ_2:54
.= ((0 + 0) + (11 * 9)) + 1 by AFINSQ_2:58
.= 100 ; :: according to NUMBER11:def 1 :: thesis: ( 100 divides value (((<%0,0%> ^ (11 --> 9)) ^ <%1%>),10) & ( for m being Nat st Sum (digits (m,10)) = 100 & 100 divides m holds
value (((<%0,0%> ^ (11 --> 9)) ^ <%1%>),10) <= m ) )
then A6: Sum ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) = 100 by Th5, A3, A4;
consider d9 being XFinSequence of NAT such that
A7: ( dom d9 = dom ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) & ( for i being Nat st i in dom d9 holds
d9 . i = (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . i) * (10 |^ i) ) & value (((<%0,0%> ^ (11 --> 9)) ^ <%1%>),10) = Sum d9 ) by NUMERAL1:def 1;
A8: (<%0,0%> ^ (11 --> 9)) ^ <%1%> = <%0,0%> ^ ((11 --> 9) ^ <%1%>) by AFINSQ_1:27;

now :: thesis: for i being Nat st i in dom d9 holds
100 divides d9 . i

let i be Nat; :: thesis: ( i in dom d9 implies 100 divides d9 . b₁ )
assume A9: i in dom d9 ; :: thesis: 100 divides d9 . b₁

per cases ( i < 1 + 1 or i >= 2 ) ;

suppose A10: i < 1 + 1 ; :: thesis: 100 divides d9 . b₁

then i <= 0 + 1 by NAT_1:9;
then ( i < 1 or i = 1 ) by NAT_1:9;
then A11: ( i = 0 or i = 1 ) by NAT_1:14;
i < len <%0,0%> by A10, AFINSQ_1:38;
then i in dom <%0,0%> by AFINSQ_1:86;
then ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . i = <%0,0%> . i by A8, ORDINAL4:def 1;
then ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . i = 0 by A11;
then d9 . i = 0 * (10 |^ i) by A9, A7;
hence 100 divides d9 . i by NAT_D:6; :: thesis: verum

end;

suppose i >= 2 ; :: thesis: 100 divides d9 . b₁

then reconsider i2 = i - 2 as Nat by NAT_1:21;
d9 . i = (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . i) * (10 |^ (i2 + 2)) by A9, A7
.= (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . i) * ((10 |^ i2) * (10 |^ 2)) by NEWTON:8
.= (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . i) * ((10 |^ i2) * (10 * 10)) by POLYEQ_5:1
.= 100 * ((((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . i) * (10 |^ i2)) ;
hence 100 divides d9 . i by INT_1:def 3; :: thesis: verum

end;

end;

end;

hence 100 divides value (((<%0,0%> ^ (11 --> 9)) ^ <%1%>),10) by A7, NUMERAL2:16; :: thesis: for m being Nat st Sum (digits (m,10)) = 100 & 100 divides m holds
value (((<%0,0%> ^ (11 --> 9)) ^ <%1%>),10) <= m
let m be Nat; :: thesis: ( Sum (digits (m,10)) = 100 & 100 divides m implies value (((<%0,0%> ^ (11 --> 9)) ^ <%1%>),10) <= m )
set dm = digits (m,10);
set dm2 = (digits (m,10)) /^ 2;
assume A12: ( Sum (digits (m,10)) = 100 & 100 divides m ) ; :: thesis: value (((<%0,0%> ^ (11 --> 9)) ^ <%1%>),10) <= m
then A13: ( (digits (m,10)) . 0 = 0 & (digits (m,10)) . 1 = 0 ) by Th13;

A14: now :: thesis: not m = 0

assume m = 0 ; :: thesis: contradiction
then digits (m,10) = <%0%> by NUMERAL1:def 2;
hence contradiction by A12, AFINSQ_2:53; :: thesis: verum

end;

assume m < value (((<%0,0%> ^ (11 --> 9)) ^ <%1%>),10) ; :: thesis: contradiction

per cases then ( len (digits (m,10)) < len (digits ((value (((<%0,0%> ^ (11 --> 9)) ^ <%1%>),10)),10)) or ( len (digits (m,10)) = len (digits ((value (((<%0,0%> ^ (11 --> 9)) ^ <%1%>),10)),10)) & ex i being Nat st
( i < len (digits (m,10)) & (digits (m,10)) . i < (digits ((value (((<%0,0%> ^ (11 --> 9)) ^ <%1%>),10)),10)) . i & ( for j being Nat st j < len (digits (m,10)) & (digits (m,10)) . j <> (digits ((value (((<%0,0%> ^ (11 --> 9)) ^ <%1%>),10)),10)) . j holds
i >= j ) ) ) ) by Th12;

suppose len (digits (m,10)) < len (digits ((value (((<%0,0%> ^ (11 --> 9)) ^ <%1%>),10)),10)) ; :: thesis: contradiction

then len (digits (m,10)) < len ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) by Th5, A3, A4;
then len (digits (m,10)) < ((len <%0,0%>) + (len (11 --> 9))) + 1 by A1, AFINSQ_1:17;
then len (digits (m,10)) < (2 + (len (11 --> 9))) + 1 by AFINSQ_1:38;
then A15: len (digits (m,10)) < 14 ;

now :: thesis: not len (digits (m,10)) < 3

assume len (digits (m,10)) < 3 ; :: thesis: contradiction
then len (digits (m,10)) in Segm 3 by NAT_1:44;
then len (digits (m,10)) in {0,1,2} by CARD_1:51;

per cases then ( len (digits (m,10)) = 0 or len (digits (m,10)) = 1 or len (digits (m,10)) = 2 ) by ENUMSET1:def 1;

suppose len (digits (m,10)) = 0 ; :: thesis: contradiction

hence contradiction by NUMERAL1:4; :: thesis: verum

end;

suppose len (digits (m,10)) = 1 ; :: thesis: contradiction

then (digits (m,10)) . (1 - 1) <> 0 by NUMERAL1:def 2, A14;
hence contradiction by Th13, A12; :: thesis: verum

end;

suppose len (digits (m,10)) = 2 ; :: thesis: contradiction

then (digits (m,10)) . (2 - 1) <> 0 by NUMERAL1:def 2, A14;
hence contradiction by Th13, A12; :: thesis: verum

end;

end;

end;

then len (digits (m,10)) >= 2 by XXREAL_0:2;
then <%((digits (m,10)) . 0),((digits (m,10)) . 1)%> = (digits (m,10)) | 2 by Th14;
then A16: digits (m,10) = <%((digits (m,10)) . 0),((digits (m,10)) . 1)%> ^ ((digits (m,10)) /^ 2) ;
then len (digits (m,10)) = (len <%((digits (m,10)) . 0),((digits (m,10)) . 1)%>) + (len ((digits (m,10)) /^ 2)) by AFINSQ_1:17;
then A17: len (digits (m,10)) = 2 + (len ((digits (m,10)) /^ 2)) by AFINSQ_1:38;
then (2 + (len ((digits (m,10)) /^ 2))) - 2 < 14 - 2 by A15, XREAL_1:14;
then len ((digits (m,10)) /^ 2) < 11 + 1 ;
then len ((digits (m,10)) /^ 2) <= 11 by NAT_1:13;
then A18: (len ((digits (m,10)) /^ 2)) * 9 <= 11 * 9 by XREAL_1:64;
A19: Sum (digits (m,10)) = (Sum <%((digits (m,10)) . 0),((digits (m,10)) . 1)%>) + (Sum ((digits (m,10)) /^ 2)) by A16, AFINSQ_2:55
.= (((digits (m,10)) . 0) + ((digits (m,10)) . 1)) + (Sum ((digits (m,10)) /^ 2)) by AFINSQ_2:54
.= (0 + ((digits (m,10)) . 1)) + (Sum ((digits (m,10)) /^ 2)) by Th13, A12
.= 0 + (Sum ((digits (m,10)) /^ 2)) by Th13, A12 ;

now :: thesis: for n being Nat st n in dom ((digits (m,10)) /^ 2) holds
((digits (m,10)) /^ 2) . n <= 9

let n be Nat; :: thesis: ( n in dom ((digits (m,10)) /^ 2) implies ((digits (m,10)) /^ 2) . n <= 9 )
assume A20: n in dom ((digits (m,10)) /^ 2) ; :: thesis: ((digits (m,10)) /^ 2) . n <= 9
then A21: ((digits (m,10)) /^ 2) . n = (digits (m,10)) . (n + 2) by AFINSQ_2:def 2;
n in Segm (dom ((digits (m,10)) /^ 2)) by A20;
then n < len ((digits (m,10)) /^ 2) by NAT_1:44;
then n + 2 < (len ((digits (m,10)) /^ 2)) + 2 by XREAL_1:8;
then n + 2 in Segm (dom (digits (m,10))) by A17, NAT_1:44;
then ((digits (m,10)) /^ 2) . n < 9 + 1 by A14, A21, NUMERAL1:def 2;
hence ((digits (m,10)) /^ 2) . n <= 9 by NAT_1:13; :: thesis: verum

end;

then Sum ((digits (m,10)) /^ 2) <= (len ((digits (m,10)) /^ 2)) * 9 by AFINSQ_2:59;
then Sum ((digits (m,10)) /^ 2) <= 11 * 9 by A18, XXREAL_0:2;
hence contradiction by A12, A19; :: thesis: verum

end;

suppose A22: ( len (digits (m,10)) = len (digits ((value (((<%0,0%> ^ (11 --> 9)) ^ <%1%>),10)),10)) & ex i being Nat st
( i < len (digits (m,10)) & (digits (m,10)) . i < (digits ((value (((<%0,0%> ^ (11 --> 9)) ^ <%1%>),10)),10)) . i & ( for j being Nat st j < len (digits (m,10)) & (digits (m,10)) . j <> (digits ((value (((<%0,0%> ^ (11 --> 9)) ^ <%1%>),10)),10)) . j holds
i >= j ) ) ) ; :: thesis: contradiction

then A23: len (digits (m,10)) = len ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) by Th5, A3, A4;
consider i being Nat such that
A24: ( i < len (digits (m,10)) & (digits (m,10)) . i < (digits ((value (((<%0,0%> ^ (11 --> 9)) ^ <%1%>),10)),10)) . i & ( for j being Nat st j < len (digits (m,10)) & (digits (m,10)) . j <> (digits ((value (((<%0,0%> ^ (11 --> 9)) ^ <%1%>),10)),10)) . j holds
i >= j ) ) by A22;

A25: now :: thesis: not i = (len ((<%0,0%> ^ (11 --> 9)) ^ <%1%>)) - 1

assume A26: i = (len ((<%0,0%> ^ (11 --> 9)) ^ <%1%>)) - 1 ; :: thesis: contradiction
then ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . i = 1 by AFINSQ_1:36, A2;
then (digits (m,10)) . i = 0 by A5, A24, NAT_1:14;
hence contradiction by A14, A26, A23, NUMERAL1:def 2; :: thesis: verum

end;

set dm1 = (digits (m,10)) | i;
set dm2 = (digits (m,10)) /^ i;
set dmi = ((digits (m,10)) /^ i) | 1;
set dmi1 = ((digits (m,10)) /^ i) /^ 1;
digits (m,10) = ((digits (m,10)) | i) ^ ((((digits (m,10)) /^ i) | 1) ^ (((digits (m,10)) /^ i) /^ 1)) ;
then Sum (digits (m,10)) = (Sum ((digits (m,10)) | i)) + (Sum ((((digits (m,10)) /^ i) | 1) ^ (((digits (m,10)) /^ i) /^ 1))) by AFINSQ_2:55;
then A27: Sum (digits (m,10)) = (Sum ((digits (m,10)) | i)) + ((Sum (((digits (m,10)) /^ i) | 1)) + (Sum (((digits (m,10)) /^ i) /^ 1))) by AFINSQ_2:55;
set d1 = ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) | i;
set d2 = ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i;
set di = (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) | 1;
set di1 = (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) /^ 1;
(<%0,0%> ^ (11 --> 9)) ^ <%1%> = (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) | i) ^ (((((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) | 1) ^ ((((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) /^ 1)) ;
then Sum ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) = (Sum (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) | i)) + (Sum (((((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) | 1) ^ ((((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) /^ 1))) by AFINSQ_2:55;
then A28: Sum ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) = (Sum (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) | i)) + ((Sum ((((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) | 1)) + (Sum ((((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) /^ 1))) by AFINSQ_2:55;
( i < len ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) & i < len (digits (m,10)) ) by A24, A5, A22;
then A29: ( len (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) = (len ((<%0,0%> ^ (11 --> 9)) ^ <%1%>)) - i & len ((digits (m,10)) /^ i) = (len (digits (m,10))) - i ) by AFINSQ_2:7;
i < len ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) by A5, A24, A22;
then i + 1 <= len ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) by NAT_1:13;
then ( i + 1 = len ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) or i + 1 < len ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) ) by XXREAL_0:1;
then i + 1 < len ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) by A25;
then (i + 1) - i < (len ((<%0,0%> ^ (11 --> 9)) ^ <%1%>)) - i by XREAL_1:9;
then A30: 1 < len (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) by A29;
then A31: len ((((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) /^ 1) = ((len ((<%0,0%> ^ (11 --> 9)) ^ <%1%>)) - i) - 1 by A29, AFINSQ_2:7;
not ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i is empty by A30;
then A32: 0 in dom (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) by AFINSQ_1:65;
i < len (digits (m,10)) by A24;
then i + 1 <= len (digits (m,10)) by NAT_1:13;
then ( i + 1 = len (digits (m,10)) or i + 1 < len (digits (m,10)) ) by XXREAL_0:1;
then i + 1 < len (digits (m,10)) by A25, A22, A5;
then (i + 1) - i < (len (digits (m,10))) - i by XREAL_1:9;
then A33: 1 < len ((digits (m,10)) /^ i) by A29;
then A34: len (((digits (m,10)) /^ i) /^ 1) = ((len (digits (m,10))) - i) - 1 by A29, AFINSQ_2:7;
not (digits (m,10)) /^ i is empty by A33;
then A35: 0 in dom ((digits (m,10)) /^ i) by AFINSQ_1:65;
A36: dom (((digits (m,10)) /^ i) /^ 1) = dom ((((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) /^ 1) by A31, A34, A22, A5;

now :: thesis: for a being Nat st a in dom (((digits (m,10)) /^ i) /^ 1) holds
(((digits (m,10)) /^ i) /^ 1) . a <= ((((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) /^ 1) . a

let a be Nat; :: thesis: ( a in dom (((digits (m,10)) /^ i) /^ 1) implies (((digits (m,10)) /^ i) /^ 1) . a <= ((((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) /^ 1) . a )
assume A37: a in dom (((digits (m,10)) /^ i) /^ 1) ; :: thesis: (((digits (m,10)) /^ i) /^ 1) . a <= ((((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) /^ 1) . a
A38: ( (((digits (m,10)) /^ i) /^ 1) . a = ((digits (m,10)) /^ i) . (a + 1) & ((((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) /^ 1) . a = (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) . (a + 1) ) by A36, A37, AFINSQ_2:def 2;
a < ((len (digits (m,10))) - i) - 1 by A34, A37, AFINSQ_1:86;
then A39: a + 1 < (((len (digits (m,10))) - i) - 1) + 1 by XREAL_1:8;
then a + 1 < len ((digits (m,10)) /^ i) by A29;
then a + 1 in dom ((digits (m,10)) /^ i) by AFINSQ_1:86;
then A40: (((digits (m,10)) /^ i) /^ 1) . a = (digits (m,10)) . ((a + 1) + i) by A38, AFINSQ_2:def 2;
a < ((len ((<%0,0%> ^ (11 --> 9)) ^ <%1%>)) - i) - 1 by A22, A5, A34, A37, AFINSQ_1:86;
then a + 1 < (((len ((<%0,0%> ^ (11 --> 9)) ^ <%1%>)) - i) - 1) + 1 by XREAL_1:8;
then a + 1 < len (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) by A29;
then a + 1 in dom (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) by AFINSQ_1:86;
then A41: ((((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) /^ 1) . a = ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . ((a + 1) + i) by A38, AFINSQ_2:def 2;
set j = (a + 1) + i;
A42: (a + 1) + i < ((len (digits (m,10))) - i) + i by A39, XREAL_1:8;
(a + 1) + i > 0 + i by XREAL_1:8;
hence (((digits (m,10)) /^ i) /^ 1) . a <= ((((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) /^ 1) . a by A41, A40, A42, A24, A5; :: thesis: verum

end;

then A43: Sum (((digits (m,10)) /^ i) /^ 1) <= Sum ((((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) /^ 1) by A36, AFINSQ_2:57;
A44: dom ((digits (m,10)) | i) = i by A24, AFINSQ_1:11
.= dom (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) | i) by A24, AFINSQ_1:11, A23 ;

now :: thesis: for a being Nat st a in dom ((digits (m,10)) | i) holds
((digits (m,10)) | i) . a <= (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) | i) . a

let a be Nat; :: thesis: ( a in dom ((digits (m,10)) | i) implies ((digits (m,10)) | i) . b₁ <= (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) | i) . b₁ )
assume A45: a in dom ((digits (m,10)) | i) ; :: thesis: ((digits (m,10)) | i) . b₁ <= (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) | i) . b₁
then a in Segm i by A24, AFINSQ_1:11;
then A46: a < i by NAT_1:44;
i < (len (<%0,0%> ^ (11 --> 9))) + 1 by A24, A1, A22, A5;
then i <= len (<%0,0%> ^ (11 --> 9)) by NAT_1:13;
then a < Segm (len (<%0,0%> ^ (11 --> 9))) by A46, XXREAL_0:2;
then A47: a in dom (<%0,0%> ^ (11 --> 9)) by NAT_1:44;
then A48: ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . a = (<%0,0%> ^ (11 --> 9)) . a by AFINSQ_1:def 3;

per cases ( a < 2 or a >= 2 ) ;

suppose a < 2 ; :: thesis: ((digits (m,10)) | i) . b₁ <= (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) | i) . b₁

then ( a = 0 or a = 1 ) by NAT_1:23;
then ( ((digits (m,10)) | i) . a = (digits (m,10)) . 0 or ((digits (m,10)) | i) . a = (digits (m,10)) . 1 ) by FUNCT_1:47, A45;
hence ((digits (m,10)) | i) . a <= (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) | i) . a by A13; :: thesis: verum

end;

suppose a >= 2 ; :: thesis: ((digits (m,10)) | i) . b₁ <= (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) | i) . b₁

then a >= len <%0,0%> by AFINSQ_1:38;
then not a in dom <%0,0%> by AFINSQ_1:86;
then consider b being Nat such that
A49: ( b in dom (11 --> 9) & a = (len <%0,0%>) + b ) by AFINSQ_1:20, A47;
((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . a = (11 --> 9) . b by A48, A49, AFINSQ_1:def 3;
then A50: ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . a = 9 by A49, FUNCOP_1:7;
dom ((digits (m,10)) | i) c= dom (digits (m,10)) by RELAT_1:60;
then a in dom (digits (m,10)) by A45;
then (digits (m,10)) . a < 9 + 1 by NUMERAL1:def 2, A14;
then (digits (m,10)) . a <= 9 by NAT_1:13;
then (digits (m,10)) . a <= ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . a by A50;
then (digits (m,10)) . a <= (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) | i) . a by A44, A45, FUNCT_1:47;
hence ((digits (m,10)) | i) . a <= (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) | i) . a by A45, FUNCT_1:47; :: thesis: verum

end;

end;

end;

then A51: Sum ((digits (m,10)) | i) <= Sum (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) | i) by A44, AFINSQ_2:57;
not (digits (m,10)) /^ i is empty by A33;
then ((digits (m,10)) /^ i) | 1 = <%(((digits (m,10)) /^ i) . 0)%> by NUMERAL2:1;
then ((digits (m,10)) /^ i) | 1 = <%((digits (m,10)) . (i + 0))%> by A35, AFINSQ_2:def 2;
then A52: Sum (((digits (m,10)) /^ i) | 1) = (digits (m,10)) . i by AFINSQ_2:53;
not ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i is empty by A30;
then (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) | 1 = <%((((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) . 0)%> by NUMERAL2:1;
then (((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) | 1 = <%(((<%0,0%> ^ (11 --> 9)) ^ <%1%>) . (i + 0))%> by A32, AFINSQ_2:def 2;
then Sum (((digits (m,10)) /^ i) | 1) < Sum ((((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) | 1) by A52, A24, A5, AFINSQ_2:53;
then (Sum (((digits (m,10)) /^ i) | 1)) + (Sum (((digits (m,10)) /^ i) /^ 1)) < (Sum ((((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) | 1)) + (Sum ((((<%0,0%> ^ (11 --> 9)) ^ <%1%>) /^ i) /^ 1)) by A43, XREAL_1:8;
then Sum (digits (m,10)) < Sum ((<%0,0%> ^ (11 --> 9)) ^ <%1%>) by A51, A27, A28, XREAL_1:8;
hence contradiction by A6, A12; :: thesis: verum

end;

end;