let x, n, k be Nat; 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 for j being Nat st j in dom (DecSD2 (x,n,k)) holds
(DecSD2 (x,n,k)) . j = (DecSD (x,n,k)) . jlet j be
Nat;
( 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))
;
(DecSD2 (x,n,k)) . j = (DecSD (x,n,k)) . jthen (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
;
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; verum