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:10
.= (1 div 1) mod (Radix k) by NEWTON:9
.= 1 mod (Radix k) by NAT_2:6 ;
hence DigA (DecSD 1,n,k),1 = 1 by A4, NAT_D:14; :: thesis: verum