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;

hence DecSD2 (x,n,k) = DecSD (x,n,k) by A1, A3, FINSEQ_2:9; :: thesis: verum

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

len (DecSD (x,n,k)) = n
by CARD_1:def 7;(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;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

hence DecSD2 (x,n,k) = DecSD (x,n,k) by A1, A3, FINSEQ_2:9; :: thesis: verum