let k, n be Nat; :: thesis: ( 1 in Seg n & k >= 2 implies DigA ((DecSD (1,n,k)),1) = 1 )
assume that
A1: 1 in Seg n and
A2: k >= 2 ; :: thesis: DigA ((DecSD (1,n,k)),1) = 1
A3: Radix k > 2 by A2, RADIX_4:1;
then A4: Radix k > 1 by XXREAL_0:2;
DigA ((DecSD (1,n,k)),1) = DigitDC (1,1,k) by A1, RADIX_1:def 9
.= (1 mod ((Radix k) |^ 1)) div ((Radix k) |^ (1 -' 1)) by RADIX_1:def 8
.= (1 div ((Radix k) |^ (1 -' 1))) mod (Radix k) by A3, RADIX_2:4
.= (1 div ((Radix k) |^ 0)) mod (Radix k) by NAT_2:8
.= (1 div 1) mod (Radix k) by NEWTON:4
.= 1 mod (Radix k) by NAT_2:4 ;
hence DigA ((DecSD (1,n,k)),1) = 1 by A4, NAT_D:14; :: thesis: verum