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

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 A2: 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 Def5, X
.= DigitDC x,j,k by RADIX_1:def 8
.= DigA (DecSD x,n,k),j by A2, X, RADIX_1:def 9
.= (DecSD x,n,k) . j by A2, X, RADIX_1:def 3 ;
hence (DecSD2 x,n,k) . j = (DecSD x,n,k) . j ; :: thesis: verum

end;

hence DecSD2 x,n,k = DecSD x,n,k by A1, FINSEQ_2:10; :: thesis: verum