reconsider d = <%0%> as XFinSequence of NAT ;

reconsider N = n, B = b as Element of NAT by ORDINAL1:def 12;

thus ( n <> 0 implies ex d being XFinSequence of NAT st

( 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 ) ) ) ) :: thesis: ( not n <> 0 implies ex b_{1} being XFinSequence of NAT st b_{1} = <%0%> )_{1} being XFinSequence of NAT st b_{1} = <%0%>

take d ; :: thesis: d = <%0%>

thus d = <%0%> ; :: thesis: verum

reconsider N = n, B = b as Element of NAT by ORDINAL1:def 12;

thus ( n <> 0 implies ex d being XFinSequence of NAT st

( 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 ) ) ) ) :: thesis: ( not n <> 0 implies ex b

proof

assume
n = 0
; :: thesis: ex b
deffunc H_{1}( Nat, Element of NAT ) -> Element of NAT = $2 div B;

consider f being sequence of NAT such that

A2: ( f . 0 = N & ( for i being Nat holds f . (i + 1) = H_{1}(i,f . i) ) )
from NAT_1:sch 12();

defpred S_{1}[ Nat] means f . $1 = 0 ;

defpred S_{2}[ Nat] means ex i being Nat st f . i = $1;

A3: for k being Nat st k <> 0 & S_{2}[k] holds

ex l being Nat st

( l < k & S_{2}[l] )
_{2}[k]
by A2;

S_{2}[ 0 ]
from NAT_1:sch 7(A7, A3);

then A8: ex l being Nat st S_{1}[l]
;

consider l being Nat such that

A9: ( S_{1}[l] & ( for i being Nat st S_{1}[i] holds

l <= i ) ) from NAT_1:sch 5(A8);

assume n <> 0 ; :: thesis: ex d being XFinSequence of NAT st

( 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 ) ) )

then consider m being Nat such that

A10: m + 1 = l by A2, A9, NAT_1:6;

reconsider m = m as Element of NAT by ORDINAL1:def 12;

dom f = NAT by FUNCT_2:def 1;

then m + 1 c= dom f by ORDINAL1:def 2;

then dom (f | (m + 1)) = m + 1 by RELAT_1:62;

then reconsider g = f | (m + 1) as XFinSequence of NAT by ORDINAL1:def 7;

defpred S_{3}[ Nat, Nat] means $2 = (g . $1) mod b;

A11: for i being Nat st i in Segm (m + 1) holds

ex x being Element of NAT st S_{3}[i,x]
;

consider d being XFinSequence of NAT such that

A12: ( dom d = Segm (m + 1) & ( for i being Nat st i in Segm (m + 1) holds

S_{3}[i,d . i] ) )
from STIRL2_1:sch 5(A11);

_{1}[l]
by A9;

A15: for i being Nat st l <= i holds

S_{1}[i]
from NAT_1:sch 8(A14, A13);

_{2}( Nat) -> set = (d . $1) * (b |^ $1);

consider d9 being XFinSequence such that

A17: ( len d9 = len d & ( for i being Nat st i in len d holds

d9 . i = H_{2}(i) ) )
from AFINSQ_1:sch 2();

rng d9 c= NAT

consider s being sequence of NAT such that

A20: s . 0 = d9 . 0 and

A21: for i being Nat st i + 1 < len d9 holds

s . (i + 1) = addnat . ((s . i),(d9 . (i + 1))) and

A22: addnat "**" d9 = s . ((len d9) - 1) by A12, A17, AFINSQ_2:def 8;

defpred S_{4}[ Nat] means ( $1 < len d9 implies s . $1 = n - ((f . ($1 + 1)) * (b |^ ($1 + 1))) );

A27: 0 in Segm (m + 1) by NAT_1:44;

then d9 . 0 = (d . 0) * (b |^ 0) by A12, A17

.= ((g . 0) mod b) * (b |^ 0) by A12, A27

.= ((f . 0) mod b) * (b |^ 0) by A27, FUNCT_1:49

.= (n mod b) * 1 by A2, NEWTON:4

.= N - (B * (N div B)) by A1, NEWTON:63

.= n - ((n div b) * (b |^ 1))

.= n - ((f . (0 + 1)) * (b |^ (0 + 1))) by A2 ;

then A28: S_{4}[ 0 ]
by A20;

for i being Nat holds S_{4}[i]
from NAT_1:sch 2(A28, A23);

then s . ld = n - ((f . (m + 1)) * (b |^ (m + 1))) by A12, A17, XREAL_1:44

.= n by A9, A10 ;

then A29: n = Sum d9 by A22, AFINSQ_2:51;

m < l by A10, NAT_1:13;

then A30: f . m <> 0 by A9;

take d ; :: thesis: ( 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 ) ) )

thus value (d,b) = n by A17, A29, Def1; :: thesis: ( d . ((len d) - 1) <> 0 & ( for i being Nat st i in dom d holds

( 0 <= d . i & d . i < b ) ) )

m in Segm (m + 1) by NAT_1:45;

then A31: g . m = f . m by FUNCT_1:49;

then ( m < m + 1 & f . (m + 1) = (g . m) div b ) by A2, NAT_1:13;

then A32: (g . m) div b = 0 by A16;

d . ((len d) - 1) = (g . m) mod b by A12, NAT_1:45

.= g . m by A1, A32, NAT_2:12, NAT_D:24 ;

hence d . ((len d) - 1) <> 0 by A30, A31; :: thesis: for i being Nat st i in dom d holds

( 0 <= d . i & d . i < b )

let i be Nat; :: thesis: ( i in dom d implies ( 0 <= d . i & d . i < b ) )

assume i in dom d ; :: thesis: ( 0 <= d . i & d . i < b )

then d . i = (g . i) mod b by A12;

hence ( 0 <= d . i & d . i < b ) by A1, NAT_D:1; :: thesis: verum

end;consider f being sequence of NAT such that

A2: ( f . 0 = N & ( for i being Nat holds f . (i + 1) = H

defpred S

defpred S

A3: for k being Nat st k <> 0 & S

ex l being Nat st

( l < k & S

proof

A7:
ex k being Nat st S
let k be Nat; :: thesis: ( k <> 0 & S_{2}[k] implies ex l being Nat st

( l < k & S_{2}[l] ) )

assume that

A4: k <> 0 and

A5: S_{2}[k]
; :: thesis: ex l being Nat st

( l < k & S_{2}[l] )

take l = k div b; :: thesis: ( l < k & S_{2}[l] )

thus l < k by A1, A4, INT_1:56; :: thesis: S_{2}[l]

consider i being Nat such that

A6: f . i = k by A5;

take i + 1 ; :: thesis: f . (i + 1) = l

thus f . (i + 1) = l by A2, A6; :: thesis: verum

end;( l < k & S

assume that

A4: k <> 0 and

A5: S

( l < k & S

take l = k div b; :: thesis: ( l < k & S

thus l < k by A1, A4, INT_1:56; :: thesis: S

consider i being Nat such that

A6: f . i = k by A5;

take i + 1 ; :: thesis: f . (i + 1) = l

thus f . (i + 1) = l by A2, A6; :: thesis: verum

S

then A8: ex l being Nat st S

consider l being Nat such that

A9: ( S

l <= i ) ) from NAT_1:sch 5(A8);

assume n <> 0 ; :: thesis: ex d being XFinSequence of NAT st

( 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 ) ) )

then consider m being Nat such that

A10: m + 1 = l by A2, A9, NAT_1:6;

reconsider m = m as Element of NAT by ORDINAL1:def 12;

dom f = NAT by FUNCT_2:def 1;

then m + 1 c= dom f by ORDINAL1:def 2;

then dom (f | (m + 1)) = m + 1 by RELAT_1:62;

then reconsider g = f | (m + 1) as XFinSequence of NAT by ORDINAL1:def 7;

defpred S

A11: for i being Nat st i in Segm (m + 1) holds

ex x being Element of NAT st S

consider d being XFinSequence of NAT such that

A12: ( dom d = Segm (m + 1) & ( for i being Nat st i in Segm (m + 1) holds

S

A13: now :: thesis: for i being Nat st l <= i & S_{1}[i] holds

S_{1}[i + 1]

A14:
SS

let i be Nat; :: thesis: ( l <= i & S_{1}[i] implies S_{1}[i + 1] )

assume l <= i ; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume S_{1}[i]
; :: thesis: S_{1}[i + 1]

then f . (i + 1) = 0 div b by A2;

hence S_{1}[i + 1]
by NAT_2:2; :: thesis: verum

end;assume l <= i ; :: thesis: ( S

assume S

then f . (i + 1) = 0 div b by A2;

hence S

A15: for i being Nat st l <= i holds

S

A16: now :: thesis: for i being Element of NAT st m < i holds

f . i = 0

deffunc Hf . i = 0

let i be Element of NAT ; :: thesis: ( m < i implies f . i = 0 )

assume m < i ; :: thesis: f . i = 0

then l <= i by A10, NAT_1:13;

hence f . i = 0 by A15; :: thesis: verum

end;assume m < i ; :: thesis: f . i = 0

then l <= i by A10, NAT_1:13;

hence f . i = 0 by A15; :: thesis: verum

consider d9 being XFinSequence such that

A17: ( len d9 = len d & ( for i being Nat st i in len d holds

d9 . i = H

rng d9 c= NAT

proof

then reconsider d9 = d9 as XFinSequence of NAT by RELAT_1:def 19;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng d9 or a in NAT )

assume a in rng d9 ; :: thesis: a in NAT

then consider i being object such that

A18: i in dom d9 and

A19: d9 . i = a by FUNCT_1:def 3;

reconsider i = i as Element of NAT by A18;

a = H_{2}(i)
by A17, A18, A19;

hence a in NAT by ORDINAL1:def 12; :: thesis: verum

end;assume a in rng d9 ; :: thesis: a in NAT

then consider i being object such that

A18: i in dom d9 and

A19: d9 . i = a by FUNCT_1:def 3;

reconsider i = i as Element of NAT by A18;

a = H

hence a in NAT by ORDINAL1:def 12; :: thesis: verum

consider s being sequence of NAT such that

A20: s . 0 = d9 . 0 and

A21: for i being Nat st i + 1 < len d9 holds

s . (i + 1) = addnat . ((s . i),(d9 . (i + 1))) and

A22: addnat "**" d9 = s . ((len d9) - 1) by A12, A17, AFINSQ_2:def 8;

defpred S

A23: now :: thesis: for i being Nat st S_{4}[i] holds

S_{4}[i + 1]

reconsider ld = (len d9) - 1 as Element of NAT by A12, A17;S

let i be Nat; :: thesis: ( S_{4}[i] implies S_{4}[i + 1] )

assume A24: S_{4}[i]
; :: thesis: S_{4}[i + 1]

_{4}[i + 1]
; :: thesis: verum

end;assume A24: S

now :: thesis: ( i + 1 < len d9 implies s . (i + 1) = n - ((f . ((i + 1) + 1)) * (b |^ ((i + 1) + 1))) )

hence
Sassume A25:
i + 1 < len d9
; :: thesis: s . (i + 1) = n - ((f . ((i + 1) + 1)) * (b |^ ((i + 1) + 1)))

then A26: i + 1 in dom d9 by AFINSQ_1:86;

thus s . (i + 1) = addnat . ((s . i),(d9 . (i + 1))) by A21, A25

.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (d9 . (i + 1)) by A24, A25, BINOP_2:def 23, NAT_1:13

.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + ((d . (i + 1)) * (b |^ (i + 1))) by A17, A26

.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((g . (i + 1)) mod b) * (b |^ (i + 1))) by A12, A17, A26

.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) mod b) * (b |^ (i + 1))) by A12, A17, A26, FUNCT_1:49

.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) - (b * ((f . (i + 1)) div B))) * (b |^ (i + 1))) by A1, NEWTON:63

.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) - (b * (f . ((i + 1) + 1)))) * (b |^ (i + 1))) by A2

.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) * (b |^ (i + 1))) - ((f . ((i + 1) + 1)) * (b * (b |^ (i + 1)))))

.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) * (b |^ (i + 1))) - ((f . ((i + 1) + 1)) * (b |^ ((i + 1) + 1)))) by NEWTON:6

.= n - ((f . ((i + 1) + 1)) * (b |^ ((i + 1) + 1))) ; :: thesis: verum

end;then A26: i + 1 in dom d9 by AFINSQ_1:86;

thus s . (i + 1) = addnat . ((s . i),(d9 . (i + 1))) by A21, A25

.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (d9 . (i + 1)) by A24, A25, BINOP_2:def 23, NAT_1:13

.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + ((d . (i + 1)) * (b |^ (i + 1))) by A17, A26

.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((g . (i + 1)) mod b) * (b |^ (i + 1))) by A12, A17, A26

.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) mod b) * (b |^ (i + 1))) by A12, A17, A26, FUNCT_1:49

.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) - (b * ((f . (i + 1)) div B))) * (b |^ (i + 1))) by A1, NEWTON:63

.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) - (b * (f . ((i + 1) + 1)))) * (b |^ (i + 1))) by A2

.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) * (b |^ (i + 1))) - ((f . ((i + 1) + 1)) * (b * (b |^ (i + 1)))))

.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) * (b |^ (i + 1))) - ((f . ((i + 1) + 1)) * (b |^ ((i + 1) + 1)))) by NEWTON:6

.= n - ((f . ((i + 1) + 1)) * (b |^ ((i + 1) + 1))) ; :: thesis: verum

A27: 0 in Segm (m + 1) by NAT_1:44;

then d9 . 0 = (d . 0) * (b |^ 0) by A12, A17

.= ((g . 0) mod b) * (b |^ 0) by A12, A27

.= ((f . 0) mod b) * (b |^ 0) by A27, FUNCT_1:49

.= (n mod b) * 1 by A2, NEWTON:4

.= N - (B * (N div B)) by A1, NEWTON:63

.= n - ((n div b) * (b |^ 1))

.= n - ((f . (0 + 1)) * (b |^ (0 + 1))) by A2 ;

then A28: S

for i being Nat holds S

then s . ld = n - ((f . (m + 1)) * (b |^ (m + 1))) by A12, A17, XREAL_1:44

.= n by A9, A10 ;

then A29: n = Sum d9 by A22, AFINSQ_2:51;

m < l by A10, NAT_1:13;

then A30: f . m <> 0 by A9;

take d ; :: thesis: ( 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 ) ) )

thus value (d,b) = n by A17, A29, Def1; :: thesis: ( d . ((len d) - 1) <> 0 & ( for i being Nat st i in dom d holds

( 0 <= d . i & d . i < b ) ) )

m in Segm (m + 1) by NAT_1:45;

then A31: g . m = f . m by FUNCT_1:49;

then ( m < m + 1 & f . (m + 1) = (g . m) div b ) by A2, NAT_1:13;

then A32: (g . m) div b = 0 by A16;

d . ((len d) - 1) = (g . m) mod b by A12, NAT_1:45

.= g . m by A1, A32, NAT_2:12, NAT_D:24 ;

hence d . ((len d) - 1) <> 0 by A30, A31; :: thesis: for i being Nat st i in dom d holds

( 0 <= d . i & d . i < b )

let i be Nat; :: thesis: ( i in dom d implies ( 0 <= d . i & d . i < b ) )

assume i in dom d ; :: thesis: ( 0 <= d . i & d . i < b )

then d . i = (g . i) mod b by A12;

hence ( 0 <= d . i & d . i < b ) by A1, NAT_D:1; :: thesis: verum

take d ; :: thesis: d = <%0%>

thus d = <%0%> ; :: thesis: verum