set d = <%6,6,2%>;
set e = <%(6 * (10 |^ 0)),(6 * (10 |^ 1)),(2 * (10 |^ 2))%>;
A1: Sum <%(6 * (10 |^ 0)),(6 * (10 |^ 1)),(2 * (10 |^ 2))%> = (Sum <%(6 * (10 |^ 0)),(6 * (10 |^ 1))%>) + (Sum <%(2 * (10 |^ 2))%>) by AFINSQ_2:55
.= ((6 * (10 |^ 0)) + (6 * (10 |^ 1))) + (Sum <%(2 * (10 |^ 2))%>) by AFINSQ_2:54
.= ((6 * (10 |^ 0)) + (6 * (10 |^ 1))) + (2 * (10 |^ 2)) by AFINSQ_2:53
.= ((6 * 1) + (6 * (10 |^ 1))) + (2 * (10 |^ 2)) by NEWTON:4
.= (6 + (6 * 10)) + (2 * (10 |^ 2)) by NEWTON:5
.= 66 + (2 * (10 * 10)) by POLYEQ_5:1
.= 266 ;
A2: dom <%6,6,2%> = 3 by AFINSQ_1:39
.= dom <%(6 * (10 |^ 0)),(6 * (10 |^ 1)),(2 * (10 |^ 2))%> by AFINSQ_1:39 ;

now :: thesis: for i being Nat st i in dom <%6,6,2%> holds
<%(6 * (10 |^ 0)),(6 * (10 |^ 1)),(2 * (10 |^ 2))%> . i = (<%6,6,2%> . i) * (10 |^ i)

let i be Nat; :: thesis: ( i in dom <%6,6,2%> implies <%(6 * (10 |^ 0)),(6 * (10 |^ 1)),(2 * (10 |^ 2))%> . i = (<%6,6,2%> . i) * (10 |^ i) )
assume i in dom <%6,6,2%> ; :: thesis: <%(6 * (10 |^ 0)),(6 * (10 |^ 1)),(2 * (10 |^ 2))%> . i = (<%6,6,2%> . i) * (10 |^ i)
then i in 3 by AFINSQ_1:39;
then i in {0,1,2} by CARD_1:51;
then ( i = 0 or i = 1 or i = 2 ) by ENUMSET1:def 1;
hence <%(6 * (10 |^ 0)),(6 * (10 |^ 1)),(2 * (10 |^ 2))%> . i = (<%6,6,2%> . i) * (10 |^ i) ; :: thesis: verum

end;

then A3: value (<%6,6,2%>,10) = 266 by A1, A2, NUMERAL1:def 1;
(len <%6,6,2%>) - 1 = 3 - 1 by AFINSQ_1:39;
then A4: <%6,6,2%> . ((len <%6,6,2%>) - 1) <> 0 ;

now :: thesis: for i being Nat st i in dom <%6,6,2%> holds
( 0 <= <%6,6,2%> . i & <%6,6,2%> . i < 10 )

let i be Nat; :: thesis: ( i in dom <%6,6,2%> implies ( 0 <= <%6,6,2%> . i & <%6,6,2%> . i < 10 ) )
assume i in dom <%6,6,2%> ; :: thesis: ( 0 <= <%6,6,2%> . i & <%6,6,2%> . i < 10 )
then i in 3 by AFINSQ_1:39;
then i in {0,1,2} by CARD_1:51;
then ( i = 0 or i = 1 or i = 2 ) by ENUMSET1:def 1;
hence ( 0 <= <%6,6,2%> . i & <%6,6,2%> . i < 10 ) ; :: thesis: verum

end;

hence digits (266,10) = <%6,6,2%> by A3, A4, NUMERAL1:def 2; :: thesis: verum