let n, m, k be Nat; :: thesis: ( n >= 1 & k >= 2 & m in Seg n 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: ( n >= 1 & k >= 2 & m in Seg n ) ; :: 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 )
assume A2: i in Seg n ; :: thesis: (DigA (SDMax n,m,k),i) + (DigA (SDMin n,m,k),i) = 0
then A3: ( i >= 1 & i <= n ) by FINSEQ_1:3;
reconsider a = SDMinDigit m,k,i as Element of INT ;
reconsider b = SDMaxDigit m,k,i as Element of INT ;
A4: DigA (SDMin n,m,k),i = SDMinDigit m,k,i by A2, Def2;

now

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