let n, b be Nat; :: thesis: ( n > 0 & b > 1 implies for i being Nat holds digits ((n * (b |^ i)),b) = (i --> 0) ^ (digits (n,b)) )
assume A1: ( n > 0 & b > 1 ) ; :: thesis: for i being Nat holds digits ((n * (b |^ i)),b) = (i --> 0) ^ (digits (n,b))
defpred S₁[ Nat] means digits ((n * (b |^ $1)),b) = ($1 --> 0) ^ (digits (n,b));
digits ((n * (b |^ 0)),b) = digits ((n * 1),b) by NEWTON:4
.= {} ^ (digits (n,b))
.= (0 --> 0) ^ (digits (n,b)) ;
then A2: S₁[ 0 ] ;

A3: now :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
digits ((n * (b |^ (i + 1))),b) = digits ((n * (b * (b |^ i))),b) by NEWTON:6
.= digits (((n * (b |^ i)) * b),b)
.= <%0%> ^ (digits ((n * (b |^ i)),b)) by A1, Th54
.= (<%0%> ^ ((Segm i) --> 0)) ^ (digits (n,b)) by A4, AFINSQ_1:27
.= ((Segm (i + 1)) --> 0) ^ (digits (n,b)) by Th53 ;
hence S₁[i + 1] ; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A3);
hence for i being Nat holds digits ((n * (b |^ i)),b) = (i --> 0) ^ (digits (n,b)) ; :: thesis: verum