let m, k be Nat; :: thesis: ( 2 <= k & m is_represented_by 1,k implies DigA_SDSub ((SD2SDSub (DecSD (m,1,k))),1) = m - ((SDSub_Add_Carry (m,k)) * (Radix k)) )

assume that

A1: 2 <= k and

A2: m is_represented_by 1,k ; :: thesis: DigA_SDSub ((SD2SDSub (DecSD (m,1,k))),1) = m - ((SDSub_Add_Carry (m,k)) * (Radix k))

A3: 1 in Seg 1 by FINSEQ_1:3;

A4: 1 in Seg (1 + 1) by FINSEQ_1:1;

then DigA_SDSub ((SD2SDSub (DecSD (m,1,k))),1) = SD2SDSubDigitS ((DecSD (m,1,k)),1,k) by RADIX_3:def 8

.= SD2SDSubDigit ((DecSD (m,1,k)),1,k) by A1, A4, RADIX_3:def 7 ;

hence DigA_SDSub ((SD2SDSub (DecSD (m,1,k))),1) = (SDSub_Add_Data ((DigA ((DecSD (m,1,k)),1)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (m,1,k)),(1 -' 1))),k)) by A3, RADIX_3:def 6

.= (SDSub_Add_Data ((DigA ((DecSD (m,1,k)),1)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (m,1,k)),0)),k)) by XREAL_1:232

.= (SDSub_Add_Data ((DigA ((DecSD (m,1,k)),1)),k)) + (SDSub_Add_Carry (0,k)) by RADIX_1:def 3

.= (SDSub_Add_Data (m,k)) + (SDSub_Add_Carry (0,k)) by A2, RADIX_1:21

.= (SDSub_Add_Data (m,k)) + 0 by RADIX_3:16

.= m - ((SDSub_Add_Carry (m,k)) * (Radix k)) by RADIX_3:def 4 ;

:: thesis: verum

assume that

A1: 2 <= k and

A2: m is_represented_by 1,k ; :: thesis: DigA_SDSub ((SD2SDSub (DecSD (m,1,k))),1) = m - ((SDSub_Add_Carry (m,k)) * (Radix k))

A3: 1 in Seg 1 by FINSEQ_1:3;

A4: 1 in Seg (1 + 1) by FINSEQ_1:1;

then DigA_SDSub ((SD2SDSub (DecSD (m,1,k))),1) = SD2SDSubDigitS ((DecSD (m,1,k)),1,k) by RADIX_3:def 8

.= SD2SDSubDigit ((DecSD (m,1,k)),1,k) by A1, A4, RADIX_3:def 7 ;

hence DigA_SDSub ((SD2SDSub (DecSD (m,1,k))),1) = (SDSub_Add_Data ((DigA ((DecSD (m,1,k)),1)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (m,1,k)),(1 -' 1))),k)) by A3, RADIX_3:def 6

.= (SDSub_Add_Data ((DigA ((DecSD (m,1,k)),1)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (m,1,k)),0)),k)) by XREAL_1:232

.= (SDSub_Add_Data ((DigA ((DecSD (m,1,k)),1)),k)) + (SDSub_Add_Carry (0,k)) by RADIX_1:def 3

.= (SDSub_Add_Data (m,k)) + (SDSub_Add_Carry (0,k)) by A2, RADIX_1:21

.= (SDSub_Add_Data (m,k)) + 0 by RADIX_3:16

.= m - ((SDSub_Add_Carry (m,k)) * (Radix k)) by RADIX_3:def 4 ;

:: thesis: verum