reconsider b1 = b - 1 as Element of NAT by A1, NAT_1:20;
let d, e be XFinSequence of NAT ; :: thesis:
thus ( n <> 0 & value (d,b) = n & d . ((len d) - 1) <> 0 & ( for i being Nat st i in dom d holds
( 0 <= d . i & d . i < b ) ) & value (e,b) = n & e . ((len e) - 1) <> 0 & ( for i being Nat st i in dom e holds
( 0 <= e . i & e . i < b ) ) implies d = e ) :: thesis:

log (2,b) > log (2,1) by A1, POWER:57;
then A33: log (2,b) > 0 by POWER:51;
log (2,b) > log (2,1) by A1, POWER:57;
then A34: log (2,b) > 0 by POWER:51;
A35: 1 - b <> 0 by A1;
A36: 1 - b <> 0 by A1;
reconsider g = (b1 (#) (b GeoSeq)) | (len d) as XFinSequence of NAT by Th1;
assume A37: n <> 0 ; :: thesis:
assume that
A38: value (d,b) = n and
A39: d . ((len d) - 1) <> 0 and
A40: for i being Nat st i in dom d holds
( 0 <= d . i & d . i < b ) ; :: thesis:
consider D being XFinSequence of NAT such that
A41: dom D = dom d and
A42: for i being Nat st i in dom D holds
D . i = (d . i) * (b |^ i) and
A43: n = Sum D by A38, Def1;
dom d <> {} by A39, FUNCT_1:def 2;
then A44: len D > 0 by A41;
A45: (len d) - 1 in dom d by A39, FUNCT_1:def 2;
then reconsider k = (len d) - 1 as Element of NAT ;
A46: 1 * (b |^ k) <= (d . k) * (b |^ k) by A39, NAT_1:4, NAT_1:14;
A47: b |^ k > 0 by A1, PREPOWER:6;
D . k = (d . k) * (b |^ k) by A41, A42, A45;
then (d . k) * (b |^ k) <= n by A41, A43, A45, A44, AFINSQ_2:61;
then b |^ k <= n by A46, XXREAL_0:2;
then log (2,(b to_power k)) <= log (2,n) by A47, PRE_FF:10;
then k * (log (2,b)) <= log (2,n) by A1, POWER:55;
then (k * (log (2,b))) / (log (2,b)) <= (log (2,n)) / (log (2,b)) by A34, XREAL_1:72;
then A48: k <= (log (2,n)) / (log (2,b)) by A34, XCMPLX_1:89;
g = ((b - 1) (#) (b GeoSeq)) | (k + 1) ;
then A49: Sum g = (Partial_Sums ((b - 1) (#) (b GeoSeq))) . k by AFINSQ_2:56
.= ((b - 1) (#) (Partial_Sums (b GeoSeq))) . k by SERIES_1:9
.= (b - 1) * ((Partial_Sums (b GeoSeq)) . k) by SEQ_1:9
.= (b - 1) * ((1 - (b to_power (k + 1))) / (1 - b)) by A1, SERIES_1:22
.= - ((1 - b) * ((1 - (b |^ (k + 1))) / (1 - b)))
.= - (1 - (b |^ (k + 1))) by A36, XCMPLX_1:87
.= (b |^ (k + 1)) - 1 ;
A50: dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def 1;
then A51: len D = len g by A41, RELAT_1:62;
len d c= dom ((b - 1) (#) (b GeoSeq)) by A50, ORDINAL1:def 2;
then A52: dom g = len d by RELAT_1:62;
A53: for i being Nat st i in dom D holds
D . i <= g . i

let i be Nat; :: thesis:
reconsider I = i as Element of NAT by ORDINAL1:def 12;
assume A54: i in dom D ; :: thesis:
then A55: D . i = (d . i) * (b |^ i) by A42;
d . i < b1 + 1 by A40, A41, A54;
then A56: d . i <= b1 by NAT_1:13;
g . I = ((b - 1) (#) (b GeoSeq)) . I by A41, A52, A54, FUNCT_1:47
.= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9
.= b1 * (b |^ I) by PREPOWER:def 1 ;
hence D . i <= g . i by A56, A55, XREAL_1:64; :: thesis:

end;

assume that
A57: value (e,b) = n and
A58: e . ((len e) - 1) <> 0 and
A59: for i being Nat st i in dom e holds
( 0 <= e . i & e . i < b ) ; :: thesis:
consider E being XFinSequence of NAT such that
A60: dom E = dom e and
A61: for i being Nat st i in dom E holds
E . i = (e . i) * (b |^ i) and
A62: n = Sum E by A57, Def1;
A63: (len e) - 1 in dom e by A58, FUNCT_1:def 2;
then reconsider l = (len e) - 1 as Element of NAT ;
A64: 1 * (b |^ l) <= (e . l) * (b |^ l) by A58, NAT_1:4, NAT_1:14;
reconsider g = (b1 (#) (b GeoSeq)) | (len e) as XFinSequence of NAT by Th1;
g = ((b - 1) (#) (b GeoSeq)) | (l + 1) ;
then A65: Sum g = (Partial_Sums ((b - 1) (#) (b GeoSeq))) . l by AFINSQ_2:56
.= ((b - 1) (#) (Partial_Sums (b GeoSeq))) . l by SERIES_1:9
.= (b - 1) * ((Partial_Sums (b GeoSeq)) . l) by SEQ_1:9
.= (b - 1) * ((1 - (b to_power (l + 1))) / (1 - b)) by A1, SERIES_1:22
.= - ((1 - b) * ((1 - (b |^ (l + 1))) / (1 - b)))
.= - (1 - (b |^ (l + 1))) by A35, XCMPLX_1:87
.= (b |^ (l + 1)) - 1 ;
dom E <> {} by A58, A60, FUNCT_1:def 2;
then A66: len E > 0 ;
A67: dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def 1;
then len e c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def 2;
then A68: dom g = len e by RELAT_1:62;
A69: for i being Nat st i in dom E holds
E . i <= g . i

proof

let i be Nat; :: thesis:
reconsider I = i as Element of NAT by ORDINAL1:def 12;
assume A70: i in dom E ; :: thesis:
then A71: E . i = (e . i) * (b |^ i) by A61;
e . i < b1 + 1 by A59, A60, A70;
then A72: e . i <= b1 by NAT_1:13;
g . I = ((b - 1) (#) (b GeoSeq)) . I by A60, A68, A70, FUNCT_1:47
.= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9
.= b1 * (b |^ I) by PREPOWER:def 1 ;
hence E . i <= g . i by A72, A71, XREAL_1:64; :: thesis:

end;

A73: b |^ l > 0 by A1, PREPOWER:6;
E . l = (e . l) * (b |^ l) by A60, A61, A63;
then (e . l) * (b |^ l) <= n by A60, A62, A63, A66, AFINSQ_2:61;
then b |^ l <= n by A64, XXREAL_0:2;
then log (2,(b to_power l)) <= log (2,n) by A73, PRE_FF:10;
then l * (log (2,b)) <= log (2,n) by A1, POWER:55;
then (l * (log (2,b))) / (log (2,b)) <= (log (2,n)) / (log (2,b)) by A33, XREAL_1:72;
then A74: l <= (log (2,n)) / (log (2,b)) by A33, XCMPLX_1:89;
len E = len g by A60, A67, RELAT_1:62;
then n < ((b |^ (l + 1)) - 1) + 1 by A62, A65, A69, AFINSQ_2:57, XREAL_1:39;
then log (2,n) < log (2,(b to_power (l + 1))) by A37, POWER:57;
then log (2,n) < (l + 1) * (log (2,b)) by A1, POWER:55;
then (log (2,n)) / (log (2,b)) < ((l + 1) * (log (2,b))) / (log (2,b)) by A33, XREAL_1:74;
then (log (2,n)) / (log (2,b)) < l + 1 by A33, XCMPLX_1:89;
then k < l + 1 by A48, XXREAL_0:2;
then A75: k <= l by NAT_1:13;
n < ((b |^ (k + 1)) - 1) + 1 by A43, A49, A51, A53, AFINSQ_2:57, XREAL_1:39;
then log (2,n) < log (2,(b to_power (k + 1))) by A37, POWER:57;
then log (2,n) < (k + 1) * (log (2,b)) by A1, POWER:55;
then (log (2,n)) / (log (2,b)) < ((k + 1) * (log (2,b))) / (log (2,b)) by A34, XREAL_1:74;
then (log (2,n)) / (log (2,b)) < k + 1 by A34, XCMPLX_1:89;
then l < k + 1 by A74, XXREAL_0:2;
then l <= k by NAT_1:13;
then A76: k = l by A75, XXREAL_0:1;

now :: thesis:

let a be object ; :: thesis:
assume A77: a in dom d ; :: thesis:
then reconsider o = a as Element of NAT ;
o < k + 1 by A77, AFINSQ_1:86;
then A78: o <= k by NAT_1:13;
A79: o < len d by A77, AFINSQ_1:86;
then reconsider oo = (len d) - o as Element of NAT by NAT_1:21;

per cases by A78, XXREAL_0:1;

suppose A80: ( o = 0 & o = k ) ; :: thesis:

then len E = 1 by A60, A76;
then A81: E = <%(E . 0)%> by AFINSQ_1:34
.= <%((e . 0) * (b |^ 0))%> by A60, A61, A76, A77, A80
.= <%((e . 0) * 1)%> by NEWTON:4 ;
len D = 1 by A41, A80;
then D = <%(D . 0)%> by AFINSQ_1:34
.= <%((d . 0) * (b |^ 0))%> by A41, A42, A77, A80
.= <%((d . 0) * 1)%> by NEWTON:4 ;
hence d . a = n by A43, A80, AFINSQ_2:53
.= e . a by A62, A80, A81, AFINSQ_2:53 ;
:: thesis:

end;

suppose A82: ( o = 0 & o < k ) ; :: thesis:

reconsider co = <%> NAT as XFinSequence of NAT ;
Sum co = 0 ;
then A83: (Sum co) div (b |^ o) = 0 by NAT_2:2;
set d9 = D;
D = co ^ D ;
then A84: n = (Sum co) + (Sum D) by A43, AFINSQ_2:55;
reconsider bo = b |^ o as Element of NAT by ORDINAL1:def 12;
A85: bo <> 0 by A1, PREPOWER:5;

A86: now :: thesis:

let k be Nat; :: thesis:
assume k in dom <%(D . o)%> ; :: thesis:
then k in Segm 1 by AFINSQ_1:33;
then k < 1 by NAT_1:44;
then k = 0 by NAT_1:14;
hence D . k = <%(D . o)%> . k by A82; :: thesis:

end;

reconsider o1 = o + 1 as Element of NAT ;
o1 <= k by A82, NAT_1:13;
then A87: o1 < len d by XREAL_1:147;
reconsider oo1 = (len d) - o1 as Element of NAT by A82;
defpred S₁[ Nat, set ] means $2 = D . ($1 + o1);
reconsider do1 = D | o1 as XFinSequence of NAT ;
A88: for u being Nat st u in Segm oo1 holds
ex x being Element of NAT st S₁[u,x] ;
consider d91 being XFinSequence of NAT such that
A89: ( dom d91 = Segm oo1 & ( for x being Nat st x in Segm oo1 holds
S₁[x,d91 . x] ) ) from STIRL2_1:sch 5(A88);
A90: len d = len D by A41;
then A91: len do1 = o1 by A87, AFINSQ_1:11;
then A92: dom D = (len do1) + (len d91) by A41, A89;

now :: thesis:

let k be Nat; :: thesis:
reconsider K = k as Element of NAT by ORDINAL1:def 12;
assume A93: k in dom d91 ; :: thesis:
then k < len d91 by AFINSQ_1:86;
then o1 + k < len D by A91, A92, XREAL_1:8;
then o1 + k in dom D by AFINSQ_1:86;
then D . (o1 + k) = (d . (o1 + k)) * (b |^ (o1 + k)) by A42;
then d91 . K = (d . (o1 + k)) * (b |^ (o1 + k)) by A89, A93
.= (d . (o1 + k)) * ((b |^ o1) * (b |^ k)) by NEWTON:8
.= ((d . (o1 + k)) * (b |^ k)) * (b |^ o1) ;
hence b |^ o1 divides d91 . k by NAT_D:def 3; :: thesis:

end;

then A94: b |^ o1 divides Sum d91 by Th2;

A95: now :: thesis:

let k be Nat; :: thesis:
assume A96: k in dom d91 ; :: thesis:
thus D . ((len <%(D . o)%>) + k) = D . ((len do1) + k) by A82, A91, AFINSQ_1:33
.= d91 . k by A89, A91, A96 ; :: thesis:

end;

dom D = 1 + (dom d91) by A41, A82, A89
.= (len <%(D . o)%>) + (len d91) by AFINSQ_1:34 ;
then D = <%(D . o)%> ^ d91 by A86, A95, AFINSQ_1:def 3;
then A97: Sum D = (Sum <%(D . o)%>) + (Sum d91) by AFINSQ_2:55;
( ( for x being Nat st x in dom do1 holds
D . x = do1 . x ) & ( for x being Nat st x in dom d91 holds
D . ((len do1) + x) = d91 . x ) ) by A89, A91, FUNCT_1:47;
then D = do1 ^ d91 by A92, AFINSQ_1:def 3;
then A98: n = (Sum do1) + (Sum d91) by A43, AFINSQ_2:55;
reconsider bo1 = b |^ o1 as Element of NAT by ORDINAL1:def 12;
consider ok1 being Nat such that
A99: ok1 + 1 = o1 ;

now :: thesis:

let k be Nat; :: thesis:
reconsider K = k as Element of NAT by ORDINAL1:def 12;
assume k in dom D ; :: thesis:
then D . K = (d . (o + k)) * (b |^ (o + k)) by A42, A82
.= (d . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8
.= ((d . (o + k)) * (b |^ k)) * (b |^ o) ;
hence b |^ o divides D . k by NAT_D:def 3; :: thesis:

end;

then A100: b |^ o divides Sum D by Th2;
then (Sum D) mod (b |^ o) = 0 by A85, PEPIN:6;
then n div (b |^ o) = ((Sum D) div (b |^ o)) + ((Sum co) div (b |^ o)) by A84, NAT_D:19;
then A101: (n div (b |^ o)) * (b |^ o) = Sum D by A83, A100, NAT_D:3;
reconsider co = <%> NAT as XFinSequence of NAT ;
Sum co = 0 ;
then A102: (Sum co) div (b |^ o) = 0 by NAT_2:2;
set d9 = E;
E = co ^ E ;
then A103: n = (Sum co) + (Sum E) by A62, AFINSQ_2:55;
reconsider bo = b |^ o as Element of NAT by ORDINAL1:def 12;
A104: bo <> 0 by A1, PREPOWER:5;
reconsider ok1 = ok1 as Element of NAT by ORDINAL1:def 12;
reconsider g1 = (b1 (#) (b GeoSeq)) | (ok1 + 1) as XFinSequence of NAT by Th1;
A105: 1 - b <> 0 by A1;
dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def 1;
then A106: o1 c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def 2;
then A107: len do1 = len g1 by A91, A99, RELAT_1:62;
A108: dom g1 = o1 by A99, A106, RELAT_1:62;
A109: for i being Nat st i in dom do1 holds
do1 . i <= g1 . i

proof

let i be Nat; :: thesis:
reconsider I = i as Element of NAT by ORDINAL1:def 12;
assume A110: i in dom do1 ; :: thesis:
then i in o1 by A87, A90, AFINSQ_1:11;
then A111: g1 . I = ((b - 1) (#) (b GeoSeq)) . I by A108, FUNCT_1:47
.= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9
.= b1 * (b |^ I) by PREPOWER:def 1 ;
A112: dom do1 c= dom D by RELAT_1:60;
then d . i < b1 + 1 by A40, A41, A110;
then A113: d . i <= b1 by NAT_1:13;
do1 . i = D . i by A110, FUNCT_1:47
.= (d . i) * (b |^ i) by A42, A110, A112 ;
hence do1 . i <= g1 . i by A111, A113, XREAL_1:64; :: thesis:

end;

now :: thesis:

let k be Nat; :: thesis:
reconsider K = k as Element of NAT by ORDINAL1:def 12;
assume k in dom E ; :: thesis:
then E . K = (e . (o + k)) * (b |^ (o + k)) by A61, A82
.= (e . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8
.= ((e . (o + k)) * (b |^ k)) * (b |^ o) ;
hence b |^ o divides E . k by NAT_D:def 3; :: thesis:

end;

A119: now :: thesis:

let k be Nat; :: thesis:
assume k in dom <%(E . o)%> ; :: thesis:
then k in Segm 1 by AFINSQ_1:33;
then k < 1 by NAT_1:44;
then k = 0 by NAT_1:14;
hence E . k = <%(E . o)%> . k by A82; :: thesis:

end;

reconsider oo1 = (len d) - o1 as Element of NAT by A82;
defpred S₂[ Nat, set ] means $2 = E . ($1 + o1);
A120: for u being Nat st u in Segm oo1 holds
ex x being Element of NAT st S₂[u,x] ;
consider d91 being XFinSequence of NAT such that
A121: ( dom d91 = Segm oo1 & ( for x being Nat st x in Segm oo1 holds
S₂[x,d91 . x] ) ) from STIRL2_1:sch 5(A120);
o1 <= k by A82, NAT_1:13;
then A122: o1 < len d by XREAL_1:147;
then A123: len do1 = o1 by A76, A116, AFINSQ_1:11;

A124: now :: thesis:

let k be Nat; :: thesis:
assume A125: k in dom d91 ; :: thesis:
thus E . ((len <%(E . o)%>) + k) = E . ((len do1) + k) by A82, A123, AFINSQ_1:33
.= d91 . k by A121, A123, A125 ; :: thesis:

end;

reconsider bo1 = b |^ o1 as Element of NAT by ORDINAL1:def 12;
consider ok1 being Nat such that
A126: ok1 + 1 = o1 ;
A127: dom E = (len do1) + (len d91) by A60, A76, A121, A123;

now :: thesis:

let k be Nat; :: thesis:
reconsider K = k as Element of NAT by ORDINAL1:def 12;
assume A128: k in dom d91 ; :: thesis:
then k < len d91 by AFINSQ_1:86;
then o1 + k < len E by A123, A127, XREAL_1:8;
then o1 + k in dom E by AFINSQ_1:86;
then E . (o1 + k) = (e . (o1 + k)) * (b |^ (o1 + k)) by A61;
then d91 . K = (e . (o1 + k)) * (b |^ (o1 + k)) by A121, A128
.= (e . (o1 + k)) * ((b |^ o1) * (b |^ k)) by NEWTON:8
.= ((e . (o1 + k)) * (b |^ k)) * (b |^ o1) ;
hence b |^ o1 divides d91 . k by NAT_D:def 3; :: thesis:

end;

then A129: b |^ o1 divides Sum d91 by Th2;
reconsider ok1 = ok1 as Element of NAT by ORDINAL1:def 12;
reconsider g1 = (b1 (#) (b GeoSeq)) | (ok1 + 1) as XFinSequence of NAT by Th1;
A130: 1 - b <> 0 by A1;
dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def 1;
then A131: o1 c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def 2;
then A132: len do1 = len g1 by A123, A126, RELAT_1:62;
A133: dom g1 = o1 by A126, A131, RELAT_1:62;
A134: for i being Nat st i in dom do1 holds
do1 . i <= g1 . i

proof

let i be Nat; :: thesis:
reconsider I = i as Element of NAT by ORDINAL1:def 12;
assume A135: i in dom do1 ; :: thesis:
then i in o1 by A76, A122, A116, AFINSQ_1:11;
then A136: g1 . I = ((b - 1) (#) (b GeoSeq)) . I by A133, FUNCT_1:47
.= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9
.= b1 * (b |^ I) by PREPOWER:def 1 ;
A137: dom do1 c= dom E by RELAT_1:60;
then e . i < b1 + 1 by A59, A60, A135;
then A138: e . i <= b1 by NAT_1:13;
do1 . i = E . i by A135, FUNCT_1:47
.= (e . i) * (b |^ i) by A61, A135, A137 ;
hence do1 . i <= g1 . i by A136, A138, XREAL_1:64; :: thesis:

end;

Sum g1 = (Partial_Sums ((b - 1) (#) (b GeoSeq))) . ok1 by AFINSQ_2:56
.= ((b - 1) (#) (Partial_Sums (b GeoSeq))) . ok1 by SERIES_1:9
.= (b - 1) * ((Partial_Sums (b GeoSeq)) . ok1) by SEQ_1:9
.= (b - 1) * ((1 - (b to_power (ok1 + 1))) / (1 - b)) by A1, SERIES_1:22
.= - ((1 - b) * ((1 - (b |^ o1)) / (1 - b))) by A126
.= - (1 - (b |^ o1)) by A130, XCMPLX_1:87
.= (b |^ o1) - 1 ;
then Sum do1 < ((b |^ o1) - 1) + 1 by A132, A134, AFINSQ_2:57, XREAL_1:145;
then A139: (Sum do1) div (b |^ o1) = 0 by NAT_D:27;
( ( for x being Nat st x in dom do1 holds
E . x = do1 . x ) & ( for x being Nat st x in dom d91 holds
E . ((len do1) + x) = d91 . x ) ) by A121, A123, FUNCT_1:47;
then E = do1 ^ d91 by A127, AFINSQ_1:def 3;
then A140: n = (Sum do1) + (Sum d91) by A62, AFINSQ_2:55;
bo1 <> 0 by A1, PREPOWER:5;
then (Sum d91) mod (b |^ o1) = 0 by A129, PEPIN:6;
then n div (b |^ o1) = ((Sum d91) div (b |^ o1)) + ((Sum do1) div (b |^ o1)) by A140, NAT_D:19;
then A141: (n div (b |^ o1)) * (b |^ o1) = Sum d91 by A139, A129, NAT_D:3;
dom E = 1 + (dom d91) by A60, A76, A82, A121
.= (len <%(E . o)%>) + (len d91) by AFINSQ_1:34 ;
then E = <%(E . o)%> ^ d91 by A119, A124, AFINSQ_1:def 3;
then Sum E = (Sum <%(E . o)%>) + (Sum d91) by AFINSQ_2:55;
then E . o = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A118, A141, AFINSQ_2:53;
then (e . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A60, A61, A76, A77;
then (e . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * ((b |^ o) * (b |^ 1))) by NEWTON:8;
then (e . o) * (b |^ o) = (b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * (b |^ 1))) ;
then ((b |^ o) * (e . o)) / (b |^ o) = ((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o) ;
hence d . a = e . a by A115, A104, XCMPLX_1:89; :: thesis:

end;

suppose A142: ( o > 0 & o = k ) ; :: thesis:

set d9 = <%(D . o)%>;
reconsider co = D | o as XFinSequence of NAT ;
A143: len d = len D by A41;
then A144: len co = o by A79, AFINSQ_1:11;
A145: len <%(D . o)%> = oo by A142, AFINSQ_1:34;
then A146: dom D = (len co) + (len <%(D . o)%>) by A41, A144;
A147: for x being Nat st x in dom <%(D . o)%> holds
D . ((len co) + x) = <%(D . o)%> . x

proof

let x be Nat; :: thesis:
assume x in dom <%(D . o)%> ; :: thesis:
then x < 1 by A142, A145, AFINSQ_1:86;
then x = 0 by NAT_1:14;
hence D . ((len co) + x) = <%(D . o)%> . x by A144; :: thesis:

end;

now :: thesis:

let k be Nat; :: thesis:
reconsider K = k as Element of NAT by ORDINAL1:def 12;
assume A148: k in dom <%(D . o)%> ; :: thesis:
then k < len <%(D . o)%> by AFINSQ_1:86;
then o + k < len D by A144, A146, XREAL_1:8;
then o + k in dom D by AFINSQ_1:86;
then D . (o + k) = (d . (o + k)) * (b |^ (o + k)) by A42;
then <%(D . o)%> . K = (d . (o + k)) * (b |^ (o + k)) by A144, A147, A148
.= (d . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8
.= ((d . (o + k)) * (b |^ k)) * (b |^ o) ;
hence b |^ o divides <%(D . o)%> . k by NAT_D:def 3; :: thesis:

end;

then A149: b |^ o divides Sum <%(D . o)%> by Th2;
reconsider bo = b |^ o as Element of NAT by ORDINAL1:def 12;
A150: 1 - b <> 0 by A1;
consider ok being Nat such that
A151: ok + 1 = o by A142, NAT_1:6;
reconsider ok = ok as Element of NAT by ORDINAL1:def 12;
reconsider g = (b1 (#) (b GeoSeq)) | (ok + 1) as XFinSequence of NAT by Th1;
A152: Sum g = (Partial_Sums ((b - 1) (#) (b GeoSeq))) . ok by AFINSQ_2:56
.= ((b - 1) (#) (Partial_Sums (b GeoSeq))) . ok by SERIES_1:9
.= (b - 1) * ((Partial_Sums (b GeoSeq)) . ok) by SEQ_1:9
.= (b - 1) * ((1 - (b to_power (ok + 1))) / (1 - b)) by A1, SERIES_1:22
.= - ((1 - b) * ((1 - (b |^ o)) / (1 - b))) by A151
.= - (1 - (b |^ o)) by A150, XCMPLX_1:87
.= (b |^ o) - 1 ;
consider ok being Nat such that
A153: ok + 1 = o by A142, NAT_1:6;
dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def 1;
then A154: o c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def 2;
then A155: dom g = o by A151, RELAT_1:62;
A156: for i being Nat st i in dom co holds
co . i <= g . i

proof

let i be Nat; :: thesis:
reconsider I = i as Element of NAT by ORDINAL1:def 12;
assume A157: i in dom co ; :: thesis:
then i in o by A79, A143, AFINSQ_1:11;
then A158: g . I = ((b - 1) (#) (b GeoSeq)) . I by A155, FUNCT_1:47
.= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9
.= b1 * (b |^ I) by PREPOWER:def 1 ;
A159: dom co c= dom D by RELAT_1:60;
then d . i < b1 + 1 by A40, A41, A157;
then A160: d . i <= b1 by NAT_1:13;
co . i = D . i by A157, FUNCT_1:47
.= (d . i) * (b |^ i) by A42, A157, A159 ;
hence co . i <= g . i by A158, A160, XREAL_1:64; :: thesis:

end;

len co = len g by A144, A151, A154, RELAT_1:62;
then Sum co < ((b |^ o) - 1) + 1 by A152, A156, AFINSQ_2:57, XREAL_1:145;
then A161: (Sum co) div (b |^ o) = 0 by NAT_D:27;
for x being Nat st x in dom co holds
D . x = co . x by FUNCT_1:47;
then D = co ^ <%(D . o)%> by A146, A147, AFINSQ_1:def 3;
then A162: n = (Sum co) + (Sum <%(D . o)%>) by A43, AFINSQ_2:55;
A163: bo <> 0 by A1, PREPOWER:5;
then (Sum <%(D . o)%>) mod (b |^ o) = 0 by A149, PEPIN:6;
then n div (b |^ o) = ((Sum <%(D . o)%>) div (b |^ o)) + ((Sum co) div (b |^ o)) by A162, NAT_D:19;
then (n div (b |^ o)) * (b |^ o) = Sum <%(D . o)%> by A161, A149, NAT_D:3;
then D . o = (n div (b |^ o)) * (b |^ o) by AFINSQ_2:53;
then ((d . o) * (b |^ o)) / (b |^ o) = ((n div (b |^ o)) * (b |^ o)) / (b |^ o) by A41, A42, A77;
then A164: d . o = ((n div (b |^ o)) * (b |^ o)) / (b |^ o) by A163, XCMPLX_1:89;
set d9 = <%(E . o)%>;
reconsider co = E | o as XFinSequence of NAT ;
A165: len e = len E by A60;
then A166: len co = o by A76, A79, AFINSQ_1:11;
A167: len <%(E . o)%> = oo by A142, AFINSQ_1:34;
then A168: dom E = (len co) + (len <%(E . o)%>) by A60, A76, A166;
A169: for x being Nat st x in dom <%(E . o)%> holds
E . ((len co) + x) = <%(E . o)%> . x

proof

let x be Nat; :: thesis:
assume x in dom <%(E . o)%> ; :: thesis:
then x < 1 by A142, A167, AFINSQ_1:86;
then x = 0 by NAT_1:14;
hence E . ((len co) + x) = <%(E . o)%> . x by A166; :: thesis:

end;

now :: thesis:

let k be Nat; :: thesis:
reconsider K = k as Element of NAT by ORDINAL1:def 12;
assume A170: k in dom <%(E . o)%> ; :: thesis:
then k < len <%(E . o)%> by AFINSQ_1:86;
then o + k < len E by A166, A168, XREAL_1:8;
then o + k in dom E by AFINSQ_1:86;
then E . (o + k) = (e . (o + k)) * (b |^ (o + k)) by A61;
then <%(E . o)%> . K = (e . (o + k)) * (b |^ (o + k)) by A166, A169, A170
.= (e . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8
.= ((e . (o + k)) * (b |^ k)) * (b |^ o) ;
hence b |^ o divides <%(E . o)%> . k by NAT_D:def 3; :: thesis:

end;

then A171: b |^ o divides Sum <%(E . o)%> by Th2;
reconsider ok = ok as Element of NAT by ORDINAL1:def 12;
reconsider g = (b1 (#) (b GeoSeq)) | (ok + 1) as XFinSequence of NAT by Th1;
reconsider bo = b |^ o as Element of NAT by ORDINAL1:def 12;
A172: 1 - b <> 0 by A1;
dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def 1;
then A173: o c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def 2;
then A174: len co = len g by A166, A153, RELAT_1:62;
A175: dom g = o by A153, A173, RELAT_1:62;
A176: for i being Nat st i in dom co holds
co . i <= g . i

proof

let i be Nat; :: thesis:
reconsider I = i as Element of NAT by ORDINAL1:def 12;
assume A177: i in dom co ; :: thesis:
then i in o by A76, A79, A165, AFINSQ_1:11;
then A178: g . I = ((b - 1) (#) (b GeoSeq)) . I by A175, FUNCT_1:47
.= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9
.= b1 * (b |^ I) by PREPOWER:def 1 ;
A179: dom co c= dom E by RELAT_1:60;
then e . i < b1 + 1 by A59, A60, A177;
then A180: e . i <= b1 by NAT_1:13;
co . i = E . i by A177, FUNCT_1:47
.= (e . i) * (b |^ i) by A61, A177, A179 ;
hence co . i <= g . i by A178, A180, XREAL_1:64; :: thesis:

end;

Sum g = (Partial_Sums ((b - 1) (#) (b GeoSeq))) . ok by AFINSQ_2:56
.= ((b - 1) (#) (Partial_Sums (b GeoSeq))) . ok by SERIES_1:9
.= (b - 1) * ((Partial_Sums (b GeoSeq)) . ok) by SEQ_1:9
.= (b - 1) * ((1 - (b to_power (ok + 1))) / (1 - b)) by A1, SERIES_1:22
.= - ((1 - b) * ((1 - (b |^ o)) / (1 - b))) by A153
.= - (1 - (b |^ o)) by A172, XCMPLX_1:87
.= (b |^ o) - 1 ;
then Sum co < ((b |^ o) - 1) + 1 by A174, A176, AFINSQ_2:57, XREAL_1:145;
then A181: (Sum co) div (b |^ o) = 0 by NAT_D:27;
for x being Nat st x in dom co holds
E . x = co . x by FUNCT_1:47;
then E = co ^ <%(E . o)%> by A168, A169, AFINSQ_1:def 3;
then A182: n = (Sum co) + (Sum <%(E . o)%>) by A62, AFINSQ_2:55;
A183: bo <> 0 by A1, PREPOWER:5;
then (Sum <%(E . o)%>) mod (b |^ o) = 0 by A171, PEPIN:6;
then n div (b |^ o) = ((Sum <%(E . o)%>) div (b |^ o)) + ((Sum co) div (b |^ o)) by A182, NAT_D:19;
then (n div (b |^ o)) * (b |^ o) = Sum <%(E . o)%> by A181, A171, NAT_D:3;
then E . o = (n div (b |^ o)) * (b |^ o) by AFINSQ_2:53;
then ((e . o) * (b |^ o)) / (b |^ o) = ((n div (b |^ o)) * (b |^ o)) / (b |^ o) by A60, A61, A76, A77;
hence d . a = e . a by A164, A183, XCMPLX_1:89; :: thesis:

end;

suppose A184: ( o > 0 & o < k ) ; :: thesis:

reconsider o1 = o + 1 as Element of NAT ;
A185: o1 <= k by A184, NAT_1:13;
then A186: o1 < len d by XREAL_1:147;
reconsider bo1 = b |^ o1 as Element of NAT by ORDINAL1:def 12;
reconsider do1 = D | o1 as XFinSequence of NAT ;
reconsider bo = b |^ o as Element of NAT by ORDINAL1:def 12;
defpred S₁[ Nat, set ] means $2 = D . ($1 + o);
consider ok1 being Nat such that
A187: ok1 + 1 = o1 ;
reconsider ok1 = ok1 as Element of NAT by ORDINAL1:def 12;
reconsider g1 = (b1 (#) (b GeoSeq)) | (ok1 + 1) as XFinSequence of NAT by Th1;
A188: len d = len D by A41;
then A189: len do1 = o1 by A186, AFINSQ_1:11;
dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def 1;
then A190: o1 c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def 2;
then A191: len do1 = len g1 by A189, A187, RELAT_1:62;
A192: dom g1 = o1 by A187, A190, RELAT_1:62;
A193: for i being Nat st i in dom do1 holds
do1 . i <= g1 . i

proof

let i be Nat; :: thesis:
reconsider I = i as Element of NAT by ORDINAL1:def 12;
assume A194: i in dom do1 ; :: thesis:
then i in o1 by A186, A188, AFINSQ_1:11;
then A195: g1 . I = ((b - 1) (#) (b GeoSeq)) . I by A192, FUNCT_1:47
.= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9
.= b1 * (b |^ I) by PREPOWER:def 1 ;
A196: dom do1 c= dom D by RELAT_1:60;
then d . i < b1 + 1 by A40, A41, A194;
then A197: d . i <= b1 by NAT_1:13;
do1 . i = D . i by A194, FUNCT_1:47
.= (d . i) * (b |^ i) by A42, A194, A196 ;
hence do1 . i <= g1 . i by A195, A197, XREAL_1:64; :: thesis:

end;

k < len d by XREAL_1:147;
then reconsider oo1 = (len d) - o1 as Element of NAT by A185, NAT_1:21, XXREAL_0:2;
A198: for u being Nat st u in Segm oo holds
ex x being Element of NAT st S₁[u,x] ;
consider d9 being XFinSequence of NAT such that
A199: ( dom d9 = Segm oo & ( for x being Nat st x in Segm oo holds
S₁[x,d9 . x] ) ) from STIRL2_1:sch 5(A198);

A200: now :: thesis:

let k be Nat; :: thesis:
assume k in dom <%(D . o)%> ; :: thesis:
then k in Segm 1 by AFINSQ_1:33;
then k < 1 by NAT_1:44;
then A201: k = 0 by NAT_1:14;
then len d9 > k by A79, XREAL_1:50, A199;
then k in dom d9 by A199, NAT_1:44;
hence d9 . k = D . (k + o) by A199
.= <%(D . o)%> . k by A201 ;
:: thesis:

end;

defpred S₂[ Nat, set ] means $2 = D . ($1 + o1);
A202: for u being Nat st u in Segm oo1 holds
ex x being Element of NAT st S₂[u,x] ;
consider d91 being XFinSequence of NAT such that
A203: ( dom d91 = Segm oo1 & ( for x being Nat st x in Segm oo1 holds
S₂[x,d91 . x] ) ) from STIRL2_1:sch 5(A202);
reconsider co = D | o as XFinSequence of NAT ;
A204: len d = len D by A41;
then A205: len co = o by A79, AFINSQ_1:11;
then A206: dom D = (len co) + (len d9) by A41, A199;

now :: thesis:

let k be Nat; :: thesis:
reconsider K = k as Element of NAT by ORDINAL1:def 12;
assume A207: k in dom d9 ; :: thesis:
then k < len d9 by AFINSQ_1:86;
then o + k < len D by A205, A206, XREAL_1:8;
then o + k in dom D by AFINSQ_1:86;
then D . (o + k) = (d . (o + k)) * (b |^ (o + k)) by A42;
then d9 . K = (d . (o + k)) * (b |^ (o + k)) by A199, A207
.= (d . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8
.= ((d . (o + k)) * (b |^ k)) * (b |^ o) ;
hence b |^ o divides d9 . k by NAT_D:def 3; :: thesis:

end;

then A208: b |^ o divides Sum d9 by Th2;
( ( for x being Nat st x in dom co holds
D . x = co . x ) & ( for x being Nat st x in dom d9 holds
D . ((len co) + x) = d9 . x ) ) by A199, A205, FUNCT_1:47;
then D = co ^ d9 by A206, AFINSQ_1:def 3;
then A209: n = (Sum co) + (Sum d9) by A43, AFINSQ_2:55;
consider ok being Nat such that
A210: ok + 1 = o by A184, NAT_1:6;
reconsider ok = ok as Element of NAT by ORDINAL1:def 12;
reconsider g = (b1 (#) (b GeoSeq)) | (ok + 1) as XFinSequence of NAT by Th1;
A211: 1 - b <> 0 by A1;
A212: Sum g = (Partial_Sums ((b - 1) (#) (b GeoSeq))) . ok by AFINSQ_2:56
.= ((b - 1) (#) (Partial_Sums (b GeoSeq))) . ok by SERIES_1:9
.= (b - 1) * ((Partial_Sums (b GeoSeq)) . ok) by SEQ_1:9
.= (b - 1) * ((1 - (b to_power (ok + 1))) / (1 - b)) by A1, SERIES_1:22
.= - ((1 - b) * ((1 - (b |^ o)) / (1 - b))) by A210
.= - (1 - (b |^ o)) by A211, XCMPLX_1:87
.= (b |^ o) - 1 ;
dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def 1;
then A213: o c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def 2;
then A214: dom g = o by A210, RELAT_1:62;
A215: for i being Nat st i in dom co holds
co . i <= g . i

proof

let i be Nat; :: thesis:
reconsider I = i as Element of NAT by ORDINAL1:def 12;
assume A216: i in dom co ; :: thesis:
then i in o by A79, A204, AFINSQ_1:11;
then A217: g . I = ((b - 1) (#) (b GeoSeq)) . I by A214, FUNCT_1:47
.= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9
.= b1 * (b |^ I) by PREPOWER:def 1 ;
A218: dom co c= dom D by RELAT_1:60;
then d . i < b1 + 1 by A40, A41, A216;
then A219: d . i <= b1 by NAT_1:13;
co . i = D . i by A216, FUNCT_1:47
.= (d . i) * (b |^ i) by A42, A216, A218 ;
hence co . i <= g . i by A217, A219, XREAL_1:64; :: thesis:

end;

A220: now :: thesis:

let k be Nat; :: thesis:
assume A221: k in dom d91 ; :: thesis:
then k < len d91 by A203, NAT_1:44;
then k + 1 < oo1 + 1 by XREAL_1:8, A203;
then k + 1 < len d9 by A199;
then A222: k + 1 in dom d9 by A199, NAT_1:44;
thus d9 . ((len <%(D . o)%>) + k) = d9 . (1 + k) by AFINSQ_1:33
.= D . ((len co) + (k + 1)) by A199, A205, A222
.= D . ((len do1) + k) by A205, A189
.= d91 . k by A203, A189, A221 ; :: thesis:

end;

dom d9 = 1 + (dom d91) by A199, A203
.= (len <%(D . o)%>) + (len d91) by AFINSQ_1:34 ;
then d9 = <%(D . o)%> ^ d91 by A200, A220, AFINSQ_1:def 3;
then A223: Sum d9 = (Sum <%(D . o)%>) + (Sum d91) by AFINSQ_2:55;
defpred S₃[ Nat, set ] means $2 = E . ($1 + o);
A224: 1 - b <> 0 by A1;
consider ok being Nat such that
A225: ok + 1 = o by A184, NAT_1:6;
A226: dom D = (len do1) + (len d91) by A41, A203, A189;

now :: thesis:

let k be Nat; :: thesis:
reconsider K = k as Element of NAT by ORDINAL1:def 12;
assume A227: k in dom d91 ; :: thesis:
then k < len d91 by AFINSQ_1:86;
then o1 + k < len D by A189, A226, XREAL_1:8;
then o1 + k in dom D by AFINSQ_1:86;
then D . (o1 + k) = (d . (o1 + k)) * (b |^ (o1 + k)) by A42;
then d91 . K = (d . (o1 + k)) * (b |^ (o1 + k)) by A203, A227
.= (d . (o1 + k)) * ((b |^ o1) * (b |^ k)) by NEWTON:8
.= ((d . (o1 + k)) * (b |^ k)) * (b |^ o1) ;
hence b |^ o1 divides d91 . k by NAT_D:def 3; :: thesis:

end;

then A228: b |^ o1 divides Sum d91 by Th2;
len co = len g by A205, A210, A213, RELAT_1:62;
then Sum co < ((b |^ o) - 1) + 1 by A212, A215, AFINSQ_2:57, XREAL_1:145;
then A229: (Sum co) div (b |^ o) = 0 by NAT_D:27;
A230: 1 - b <> 0 by A1;
Sum g1 = (Partial_Sums ((b - 1) (#) (b GeoSeq))) . ok1 by AFINSQ_2:56
.= ((b - 1) (#) (Partial_Sums (b GeoSeq))) . ok1 by SERIES_1:9
.= (b - 1) * ((Partial_Sums (b GeoSeq)) . ok1) by SEQ_1:9
.= (b - 1) * ((1 - (b to_power (ok1 + 1))) / (1 - b)) by A1, SERIES_1:22
.= - ((1 - b) * ((1 - (b |^ o1)) / (1 - b))) by A187
.= - (1 - (b |^ o1)) by A230, XCMPLX_1:87
.= (b |^ o1) - 1 ;
then Sum do1 < ((b |^ o1) - 1) + 1 by A191, A193, AFINSQ_2:57, XREAL_1:145;
then A231: (Sum do1) div (b |^ o1) = 0 by NAT_D:27;
( ( for x being Nat st x in dom do1 holds
D . x = do1 . x ) & ( for x being Nat st x in dom d91 holds
D . ((len do1) + x) = d91 . x ) ) by A203, A189, FUNCT_1:47;
then D = do1 ^ d91 by A226, AFINSQ_1:def 3;
then A232: n = (Sum do1) + (Sum d91) by A43, AFINSQ_2:55;
bo1 <> 0 by A1, PREPOWER:5;
then (Sum d91) mod (b |^ o1) = 0 by A228, PEPIN:6;
then n div (b |^ o1) = ((Sum d91) div (b |^ o1)) + ((Sum do1) div (b |^ o1)) by A232, NAT_D:19;
then A233: (n div (b |^ o1)) * (b |^ o1) = Sum d91 by A231, A228, NAT_D:3;
A234: bo <> 0 by A1, PREPOWER:5;
then (Sum d9) mod (b |^ o) = 0 by A208, PEPIN:6;
then n div (b |^ o) = ((Sum d9) div (b |^ o)) + ((Sum co) div (b |^ o)) by A209, NAT_D:19;
then ( (n div (b |^ o)) * (b |^ o) = Sum d9 & Sum <%(D . o)%> = D . o ) by A229, A208, AFINSQ_2:53, NAT_D:3;
then (d . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A41, A42, A77, A233, A223;
then (d . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * ((b |^ o) * (b |^ 1))) by NEWTON:8;
then (d . o) * (b |^ o) = (b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * (b |^ 1))) ;
then ((b |^ o) * (d . o)) / (b |^ o) = ((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o) ;
then A235: d . o = ((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o) by A234, XCMPLX_1:89;
reconsider o1 = o + 1 as Element of NAT ;
A236: o1 <= k by A184, NAT_1:13;
then A237: o1 < len d by XREAL_1:147;
reconsider ok = ok as Element of NAT by ORDINAL1:def 12;
reconsider g = (b1 (#) (b GeoSeq)) | (ok + 1) as XFinSequence of NAT by Th1;
A238: 1 - b <> 0 by A1;
reconsider bo1 = b |^ o1 as Element of NAT by ORDINAL1:def 12;
reconsider do1 = E | o1 as XFinSequence of NAT ;
reconsider bo = b |^ o as Element of NAT by ORDINAL1:def 12;
consider ok1 being Nat such that
A239: ok1 + 1 = o1 ;
reconsider ok1 = ok1 as Element of NAT by ORDINAL1:def 12;
reconsider g1 = (b1 (#) (b GeoSeq)) | (ok1 + 1) as XFinSequence of NAT by Th1;
A240: len e = len E by A60;
then A241: len do1 = o1 by A76, A237, AFINSQ_1:11;
dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def 1;
then A242: o1 c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def 2;
then A243: len do1 = len g1 by A241, A239, RELAT_1:62;
A244: dom g1 = o1 by A239, A242, RELAT_1:62;
A245: for i being Nat st i in dom do1 holds
do1 . i <= g1 . i

proof

let i be Nat; :: thesis:
reconsider I = i as Element of NAT by ORDINAL1:def 12;
assume A246: i in dom do1 ; :: thesis:
then i in o1 by A76, A237, A240, AFINSQ_1:11;
then A247: g1 . I = ((b - 1) (#) (b GeoSeq)) . I by A244, FUNCT_1:47
.= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9
.= b1 * (b |^ I) by PREPOWER:def 1 ;
A248: dom do1 c= dom E by RELAT_1:60;
then e . i < b1 + 1 by A59, A60, A246;
then A249: e . i <= b1 by NAT_1:13;
do1 . i = E . i by A246, FUNCT_1:47
.= (e . i) * (b |^ i) by A61, A246, A248 ;
hence do1 . i <= g1 . i by A247, A249, XREAL_1:64; :: thesis:

end;

A253: now :: thesis:

let k be Nat; :: thesis:
assume k in dom <%(E . o)%> ; :: thesis:
then k in Segm 1 by AFINSQ_1:33;
then k < 1 by NAT_1:44;
then A254: k = 0 by NAT_1:14;
oo > 0 by A79, XREAL_1:50;
then k < len d9 by A252, A254;
then k in dom d9 by A252, NAT_1:44;
hence d9 . k = E . (k + o) by A252
.= <%(E . o)%> . k by A254 ;
:: thesis:

end;

defpred S₄[ Nat, set ] means $2 = E . ($1 + o1);
A255: for u being Nat st u in Segm oo1 holds
ex x being Element of NAT st S₄[u,x] ;
consider d91 being XFinSequence of NAT such that
A256: ( dom d91 = Segm oo1 & ( for x being Nat st x in Segm oo1 holds
S₄[x,d91 . x] ) ) from STIRL2_1:sch 5(A255);
A257: dom E = (len do1) + (len d91) by A60, A76, A256, A241;

now :: thesis:

let k be Nat; :: thesis:
reconsider K = k as Element of NAT by ORDINAL1:def 12;
assume A258: k in dom d91 ; :: thesis:
then k < len d91 by AFINSQ_1:86;
then o1 + k < len E by A241, A257, XREAL_1:8;
then o1 + k in dom E by AFINSQ_1:86;
then E . (o1 + k) = (e . (o1 + k)) * (b |^ (o1 + k)) by A61;
then d91 . K = (e . (o1 + k)) * (b |^ (o1 + k)) by A256, A258
.= (e . (o1 + k)) * ((b |^ o1) * (b |^ k)) by NEWTON:8
.= ((e . (o1 + k)) * (b |^ k)) * (b |^ o1) ;
hence b |^ o1 divides d91 . k by NAT_D:def 3; :: thesis:

end;

then A259: b |^ o1 divides Sum d91 by Th2;
( ( for x being Nat st x in dom do1 holds
E . x = do1 . x ) & ( for x being Nat st x in dom d91 holds
E . ((len do1) + x) = d91 . x ) ) by A256, A241, FUNCT_1:47;
then E = do1 ^ d91 by A257, AFINSQ_1:def 3;
then A260: n = (Sum do1) + (Sum d91) by A62, AFINSQ_2:55;
bo1 <> 0 by A1, PREPOWER:5;
then (Sum d91) mod (b |^ o1) = 0 by A259, PEPIN:6;
then n div (b |^ o1) = ((Sum d91) div (b |^ o1)) + ((Sum do1) div (b |^ o1)) by A260, NAT_D:19;
then A261: (n div (b |^ o1)) * (b |^ o1) = Sum d91 by A250, A259, NAT_D:3;
reconsider co = E | o as XFinSequence of NAT ;
A262: len e = len E by A60;
then A263: len co = o by A76, A79, AFINSQ_1:11;
then A264: dom E = (len co) + (len d9) by A60, A76, A252;

now :: thesis:

let k be Nat; :: thesis:
reconsider K = k as Element of NAT by ORDINAL1:def 12;
assume A265: k in dom d9 ; :: thesis:
then k < len d9 by AFINSQ_1:86;
then o + k < len E by A263, A264, XREAL_1:8;
then o + k in dom E by AFINSQ_1:86;
then E . (o + k) = (e . (o + k)) * (b |^ (o + k)) by A61;
then d9 . K = (e . (o + k)) * (b |^ (o + k)) by A252, A265
.= (e . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8
.= ((e . (o + k)) * (b |^ k)) * (b |^ o) ;
hence b |^ o divides d9 . k by NAT_D:def 3; :: thesis:

end;

then A266: b |^ o divides Sum d9 by Th2;
dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def 1;
then A267: o c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def 2;
then A268: len co = len g by A263, A225, RELAT_1:62;
A269: dom g = o by A225, A267, RELAT_1:62;
A270: for i being Nat st i in dom co holds
co . i <= g . i

proof

let i be Nat; :: thesis:
reconsider I = i as Element of NAT by ORDINAL1:def 12;
assume A271: i in dom co ; :: thesis:
then i in o by A76, A79, A262, AFINSQ_1:11;
then A272: g . I = ((b - 1) (#) (b GeoSeq)) . I by A269, FUNCT_1:47
.= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9
.= b1 * (b |^ I) by PREPOWER:def 1 ;
A273: dom co c= dom E by RELAT_1:60;
then e . i < b1 + 1 by A59, A60, A271;
then A274: e . i <= b1 by NAT_1:13;
co . i = E . i by A271, FUNCT_1:47
.= (e . i) * (b |^ i) by A61, A271, A273 ;
hence co . i <= g . i by A272, A274, XREAL_1:64; :: thesis:

end;

A276: now :: thesis:

let k be Nat; :: thesis:
assume A277: k in dom d91 ; :: thesis:
then k < len d91 by A256, NAT_1:44;
then k + 1 < oo1 + 1 by XREAL_1:8, A256;
then A278: k + 1 in Segm oo by NAT_1:44;
thus d9 . ((len <%(E . o)%>) + k) = d9 . (1 + k) by AFINSQ_1:33
.= E . ((len co) + (k + 1)) by A252, A263, A278
.= E . ((len do1) + k) by A263, A241
.= d91 . k by A256, A241, A277 ; :: thesis:

end;

end;

hence d = e by A76, FUNCT_1:2; :: thesis:

end;

assume that
n = 0 and
A282: ( d = <%0%> & e = <%0%> ) ; :: thesis:
thus d = e by A282; :: thesis: