let x, n, k be Nat; :: thesis: DecSD2 x,n,k = DecSD x,n,k
A1: len (DecSD2 x,n,k) = n by FINSEQ_1:def 18;
then A2: dom (DecSD2 x,n,k) = Seg n by FINSEQ_1:def 3;

A3: now

let j be Nat; :: thesis: ( j in dom (DecSD2 x,n,k) implies (DecSD2 x,n,k) . j = (DecSD x,n,k) . j )
assume A4: j in dom (DecSD2 x,n,k) ; :: thesis: (DecSD2 x,n,k) . j = (DecSD x,n,k) . j
then (DecSD2 x,n,k) . j = DigitDC2 x,j,k by A2, Def5
.= DigitDC x,j,k by RADIX_1:def 8
.= DigA (DecSD x,n,k),j by A2, A4, RADIX_1:def 9
.= (DecSD x,n,k) . j by A2, A4, RADIX_1:def 3 ;
hence (DecSD2 x,n,k) . j = (DecSD x,n,k) . j ; :: thesis: verum

end;

len (DecSD x,n,k) = n by FINSEQ_1:def 18;
hence DecSD2 x,n,k = DecSD x,n,k by A1, A3, FINSEQ_2:10; :: thesis: verum