set d = <%9,1%>;
set e = <%(9 * (10 |^ 0)),(1 * (10 |^ 1))%>;
A1: Sum <%(9 * (10 |^ 0)),(1 * (10 |^ 1))%> = (9 * (10 |^ 0)) + (1 * (10 |^ 1)) by AFINSQ_2:54
.= (9 * 1) + (1 * (10 |^ 1)) by NEWTON:4
.= 9 + (1 * 10) by NEWTON:5 ;
A2: dom <%9,1%> = 2 by AFINSQ_1:38
.= dom <%(9 * (10 |^ 0)),(1 * (10 |^ 1))%> by AFINSQ_1:38 ;

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

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

end;

then A3: value (<%9,1%>,10) = 19 by A1, A2, NUMERAL1:def 1;
(len <%9,1%>) - 1 = 2 - 1 by AFINSQ_1:38;
then A4: <%9,1%> . ((len <%9,1%>) - 1) <> 0 ;

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

let i be Nat; :: thesis: ( i in dom <%9,1%> implies ( 0 <= <%9,1%> . i & <%9,1%> . i < 10 ) )
assume i in dom <%9,1%> ; :: thesis: ( 0 <= <%9,1%> . i & <%9,1%> . i < 10 )
then i in 2 by AFINSQ_1:38;
then i in {0,1} by CARD_1:50;
then ( i = 0 or i = 1 ) by TARSKI:def 2;
hence ( 0 <= <%9,1%> . i & <%9,1%> . i < 10 ) ; :: thesis: verum

end;

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