let x, n, k be Nat; :: thesis: DecSD2 (x,n,k) = DecSD (x,n,k)
A1: len (DecSD2 (x,n,k)) = n by CARD_1:def 7;
then A2: dom (DecSD2 (x,n,k)) = Seg n by FINSEQ_1:def 3;
A3: now :: thesis: for j being Nat st j in dom (DecSD2 (x,n,k)) holds
(DecSD2 (x,n,k)) . j = (DecSD (x,n,k)) . j
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 CARD_1:def 7;
hence DecSD2 (x,n,k) = DecSD (x,n,k) by A1, A3, FINSEQ_2:9; :: thesis: verum