let n, m, k be Nat; :: thesis: ( k >= 2 implies for i being Nat st i in Seg n holds
(DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0 )
assume A1: k >= 2 ; :: thesis: for i being Nat st i in Seg n holds
(DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0
let i be Nat; :: thesis: ( i in Seg n implies (DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0 )
reconsider a = SDMinDigit (m,k,i) as Element of INT ;
reconsider b = SDMaxDigit (m,k,i) as Element of INT ;
assume A2: i in Seg n ; :: thesis: (DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0
then A3: i >= 1 by FINSEQ_1:1;
A4: DigA ((SDMin (n,m,k)),i) = SDMinDigit (m,k,i) by A2, Def2;

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

per cases ( i < m or i >= m ) ;

suppose A5: i < m ; :: thesis: (DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0

then a + b = ((- (Radix k)) + 1) + b by A1, A3, Def1
.= ((- (Radix k)) + 1) + ((Radix k) - 1) by A1, A3, A5, Def3
.= 0 ;
hence (DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0 by A2, A4, Def4; :: thesis: verum

end;

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

then a + b = 0 + b by A1, Def1
.= 0 + 0 by A1, A6, Def3 ;
hence (DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0 by A2, A4, Def4; :: thesis: verum

end;

end;

end;

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