let n be Nat; :: thesis: ( n >= 1 implies for m, k being Nat st k >= 2 holds
(SDDec (SDMax (n,m,k))) + (SDDec (SDMin (n,m,k))) = SDDec (DecSD (0,n,k)) )
assume A1: n >= 1 ; :: thesis: for m, k being Nat st k >= 2 holds
(SDDec (SDMax (n,m,k))) + (SDDec (SDMin (n,m,k))) = SDDec (DecSD (0,n,k))
then A2: n in Seg n by FINSEQ_1:1;
let m, k be Nat; :: thesis: ( k >= 2 implies (SDDec (SDMax (n,m,k))) + (SDDec (SDMin (n,m,k))) = SDDec (DecSD (0,n,k)) )
assume A3: k >= 2 ; :: thesis: (SDDec (SDMax (n,m,k))) + (SDDec (SDMin (n,m,k))) = SDDec (DecSD (0,n,k))
A4: for i being Nat st i in Seg n holds
DigA ((DecSD (0,n,k)),i) = DigA (((SDMax (n,m,k)) '+' (SDMin (n,m,k))),i)

proof

let i be Nat; :: thesis: ( i in Seg n implies DigA ((DecSD (0,n,k)),i) = DigA (((SDMax (n,m,k)) '+' (SDMin (n,m,k))),i) )
assume A5: i in Seg n ; :: thesis: DigA ((DecSD (0,n,k)),i) = DigA (((SDMax (n,m,k)) '+' (SDMin (n,m,k))),i)
then A6: DigA (((SDMax (n,m,k)) '+' (SDMin (n,m,k))),i) = Add ((SDMax (n,m,k)),(SDMin (n,m,k)),i,k) by RADIX_1:def 14
.= (SD_Add_Data (((DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i))),k)) + (SD_Add_Carry ((DigA ((SDMax (n,m,k)),(i -' 1))) + (DigA ((SDMin (n,m,k)),(i -' 1))))) by A3, A5, RADIX_1:def 13
.= (SD_Add_Data (0,k)) + (SD_Add_Carry ((DigA ((SDMax (n,m,k)),(i -' 1))) + (DigA ((SDMin (n,m,k)),(i -' 1))))) by A3, A5, Th16
.= 0 + (SD_Add_Carry ((DigA ((SDMax (n,m,k)),(i -' 1))) + (DigA ((SDMin (n,m,k)),(i -' 1))))) by RADIX_1:19 ;
A7: DigA ((DecSD (0,n,k)),i) = 0 by A5, Th5;
A8: i >= 1 by A5, FINSEQ_1:1;

now :: thesis: DigA ((DecSD (0,n,k)),i) = DigA (((SDMax (n,m,k)) '+' (SDMin (n,m,k))),i)

per cases ( i = 1 or i > 1 ) by A8, XXREAL_0:1;

suppose A9: i = 1 ; :: thesis: DigA ((DecSD (0,n,k)),i) = DigA (((SDMax (n,m,k)) '+' (SDMin (n,m,k))),i)

then DigA ((SDMin (n,m,k)),(i -' 1)) = 0 by NAT_2:8, RADIX_1:def 3;
then DigA (((SDMax (n,m,k)) '+' (SDMin (n,m,k))),i) = SD_Add_Carry (0 + 0) by A6, A9, NAT_2:8, RADIX_1:def 3;
hence DigA ((DecSD (0,n,k)),i) = DigA (((SDMax (n,m,k)) '+' (SDMin (n,m,k))),i) by A7, RADIX_1:def 10; :: thesis: verum

end;

suppose i > 1 ; :: thesis: DigA ((DecSD (0,n,k)),i) = DigA (((SDMax (n,m,k)) '+' (SDMin (n,m,k))),i)

then i -' 1 in Seg n by A5, Th2;
then DigA (((SDMax (n,m,k)) '+' (SDMin (n,m,k))),i) = SD_Add_Carry 0 by A3, A6, Th16;
hence DigA ((DecSD (0,n,k)),i) = DigA (((SDMax (n,m,k)) '+' (SDMin (n,m,k))),i) by A7, RADIX_1:def 10; :: thesis: verum

end;

end;

end;

hence DigA ((DecSD (0,n,k)),i) = DigA (((SDMax (n,m,k)) '+' (SDMin (n,m,k))),i) ; :: thesis: verum

end;

(SDDec (SDMax (n,m,k))) + (SDDec (SDMin (n,m,k))) = (SDDec ((SDMax (n,m,k)) '+' (SDMin (n,m,k)))) + ((SD_Add_Carry ((DigA ((SDMax (n,m,k)),n)) + (DigA ((SDMin (n,m,k)),n)))) * ((Radix k) |^ n)) by A1, A3, RADIX_2:11
.= (SDDec ((SDMax (n,m,k)) '+' (SDMin (n,m,k)))) + ((SD_Add_Carry 0) * ((Radix k) |^ n)) by A3, A2, Th16
.= (SDDec ((SDMax (n,m,k)) '+' (SDMin (n,m,k)))) + (0 * ((Radix k) |^ n)) by RADIX_1:def 10 ;
hence (SDDec (SDMax (n,m,k))) + (SDDec (SDMin (n,m,k))) = SDDec (DecSD (0,n,k)) by A1, A4, Th12; :: thesis: verum