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

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

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

end;

then A3: value (<%4,3,0,1%>,10) = 1034 by A1, A2, NUMERAL1:def 1;
(len <%4,3,0,1%>) - 1 = 4 - 1 by AFINSQ_1:84;
then A4: <%4,3,0,1%> . ((len <%4,3,0,1%>) - 1) <> 0 ;

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

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

end;

hence digits (1034,10) = <%4,3,0,1%> by A3, A4, NUMERAL1:def 2; :: thesis: verum