:: RADIX_4 semantic presentation

begin


theorem Th1: :: RADIX_4:1
for k being Nat st 2 <= k holds
2 < Radix k
proof
let k be Nat; ::_thesis: ( 2 <= k implies 2 < Radix k )
defpred S1[ Nat] means 2 < Radix $1;
A1: for kk being Nat st kk >= 2 & S1[kk] holds
S1[kk + 1]
proof
let kk be Nat; ::_thesis: ( kk >= 2 & S1[kk] implies S1[kk + 1] )
assume that
 2 <= kk and
A2: 2 < Radix kk ; ::_thesis: S1[kk + 1]
A3: Radix (kk + 1) = (2 to_power 1) * (2 to_power kk) by POWER:27
.= 2 * (Radix kk) by POWER:25 ;
 Radix kk > 1 by A2, XXREAL_0:2;
hence  S1[kk + 1] by A3, XREAL_1:155; ::_thesis: verum
end;
Radix 2 = 2 to_power (1 + 1)
.= (2 to_power 1) * (2 to_power 1) by POWER:27
.= 2 * (2 to_power 1) by POWER:25
.= 2 * 2 by POWER:25
.= 4 ;
then A4: S1[2] ;
 for k being Nat st 2 <= k holds
S1[k] from NAT_1:sch_8(A4, A1);
hence  ( 2 <= k implies 2 < Radix k ) ; ::_thesis: verum
end;

Lm1:  for k being Nat
for i1 being Integer st i1 in k -SD_Sub_S holds
( i1 >= - (Radix (k -' 1)) & i1 <= (Radix (k -' 1)) - 1 )
proof
let k be Nat; ::_thesis: for i1 being Integer st i1 in k -SD_Sub_S holds
( i1 >= - (Radix (k -' 1)) & i1 <= (Radix (k -' 1)) - 1 )
let i1 be Integer; ::_thesis: ( i1 in k -SD_Sub_S implies ( i1 >= - (Radix (k -' 1)) & i1 <= (Radix (k -' 1)) - 1 ) )
A1: k -SD_Sub_S =  {  e where e is Element of INT : ( - (Radix (k -' 1)) <= e & e <= (Radix (k -' 1)) - 1 )  }  by RADIX_3:def_1;
assume  i1 in k -SD_Sub_S ; ::_thesis: ( i1 >= - (Radix (k -' 1)) & i1 <= (Radix (k -' 1)) - 1 )
then  ex i being Element of INT st
( i = i1 & - (Radix (k -' 1)) <= i & i <= (Radix (k -' 1)) - 1 ) by A1;
hence  ( i1 >= - (Radix (k -' 1)) & i1 <= (Radix (k -' 1)) - 1 ) ; ::_thesis: verum
end;

Lm2:  for n, m, k, i being Nat st i in Seg n holds
DigA ((DecSD (m,(n + 1),k)),i) = DigA ((DecSD (m,n,k)),i)
proof
let n, m, k, i be Nat; ::_thesis: ( i in Seg n implies DigA ((DecSD (m,(n + 1),k)),i) = DigA ((DecSD (m,n,k)),i) )
assume A1: i in Seg n ; ::_thesis: DigA ((DecSD (m,(n + 1),k)),i) = DigA ((DecSD (m,n,k)),i)
then  i <= n by FINSEQ_1:1;
then A2: i <= n + 1 by NAT_1:12;
 1 <= i by A1, FINSEQ_1:1;
then A3: i in Seg (n + 1) by A2, FINSEQ_1:1;
DigA ((DecSD (m,n,k)),i) = DigitDC (m,i,k) by A1, RADIX_1:def_9
.= DigA ((DecSD (m,(n + 1),k)),i) by A3, RADIX_1:def_9 ;
hence  DigA ((DecSD (m,(n + 1),k)),i) = DigA ((DecSD (m,n,k)),i) ; ::_thesis: verum
end;

Lm3:  for k, x, n being Nat st n >= 1 holds
DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),n) = DigA ((DecSD (x,n,k)),n)
proof
let k, x, n be Nat; ::_thesis: ( n >= 1 implies DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),n) = DigA ((DecSD (x,n,k)),n) )
set xn = x mod ((Radix k) |^ n);
assume  n >= 1 ; ::_thesis: DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),n) = DigA ((DecSD (x,n,k)),n)
then  n <> 0 ;
then A1: n in Seg n by FINSEQ_1:3;
then  DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),n) = DigitDC ((x mod ((Radix k) |^ n)),n,k) by RADIX_1:def_9
.= DigitDC (x,n,k) by EULER_2:5
.= DigA ((DecSD (x,n,k)),n) by A1, RADIX_1:def_9 ;
hence  DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),n) = DigA ((DecSD (x,n,k)),n) ; ::_thesis: verum
end;

begin

theorem Th2: :: RADIX_4:2
for x, y being Integer
for k being Nat st 3 <= k holds
SDSub_Add_Carry (((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))),k) = 0
proof
let x, y be Integer; ::_thesis: for k being Nat st 3 <= k holds
SDSub_Add_Carry (((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))),k) = 0
let k be Nat; ::_thesis: ( 3 <= k implies SDSub_Add_Carry (((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))),k) = 0 )
set CC = (SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k));
 ( - 1 <= SDSub_Add_Carry (x,k) & - 1 <= SDSub_Add_Carry (y,k) ) by RADIX_3:12;
then A1: (- 1) + (- 1) <= (SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k)) by XREAL_1:7;
assume  k >= 3 ; ::_thesis: SDSub_Add_Carry (((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))),k) = 0
then A2: k - 1 >= 3 - 1 by XREAL_1:13;
then  k - 1 > 0 by XXREAL_0:2;
then  k - 1 = k -' 1 by XREAL_0:def_2;
then A3: Radix (k -' 1) > 2 by A2, Th1;
 ( SDSub_Add_Carry (x,k) <= 1 & SDSub_Add_Carry (y,k) <= 1 ) by RADIX_3:12;
then  (SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k)) <= 1 + 1 by XREAL_1:7;
then A4: (SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k)) < Radix (k -' 1) by A3, XXREAL_0:2;
 - (Radix (k -' 1)) <= - 2 by A3, XREAL_1:24;
then  - (Radix (k -' 1)) <= (SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k)) by A1, XXREAL_0:2;
hence  SDSub_Add_Carry (((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))),k) = 0 by A4, RADIX_3:def_3; ::_thesis: verum
end;

theorem Th3: :: RADIX_4:3
for k, m, n being Nat st 2 <= k holds
DigA_SDSub ((SD2SDSub (DecSD (m,n,k))),(n + 1)) = SDSub_Add_Carry ((DigA ((DecSD (m,n,k)),n)),k)
proof
let k, m, n be Nat; ::_thesis: ( 2 <= k implies DigA_SDSub ((SD2SDSub (DecSD (m,n,k))),(n + 1)) = SDSub_Add_Carry ((DigA ((DecSD (m,n,k)),n)),k) )
assume A1: 2 <= k ; ::_thesis: DigA_SDSub ((SD2SDSub (DecSD (m,n,k))),(n + 1)) = SDSub_Add_Carry ((DigA ((DecSD (m,n,k)),n)),k)
 0 <= n by NAT_1:2;
then  0 + 1 <= n + 1 by XREAL_1:7;
then A2: n + 1 in Seg (n + 1) by FINSEQ_1:1;
hence  DigA_SDSub ((SD2SDSub (DecSD (m,n,k))),(n + 1)) = SD2SDSubDigitS ((DecSD (m,n,k)),(n + 1),k) by RADIX_3:def_8
.= SD2SDSubDigit ((DecSD (m,n,k)),(n + 1),k) by A1, A2, RADIX_3:def_7
.= SDSub_Add_Carry ((DigA ((DecSD (m,n,k)),((n + 1) -' 1))),k) by RADIX_3:def_6
.= SDSub_Add_Carry ((DigA ((DecSD (m,n,k)),n)),k) by NAT_D:34 ;
::_thesis: verum
end;

theorem Th4: :: RADIX_4:4
for k, m being Nat st 2 <= k & m is_represented_by 1,k holds
DigA_SDSub ((SD2SDSub (DecSD (m,1,k))),(1 + 1)) = SDSub_Add_Carry (m,k)
proof
let k, m be Nat; ::_thesis: ( 2 <= k & m is_represented_by 1,k implies DigA_SDSub ((SD2SDSub (DecSD (m,1,k))),(1 + 1)) = SDSub_Add_Carry (m,k) )
assume that
A1: 2 <= k and
A2: m is_represented_by 1,k ; ::_thesis: DigA_SDSub ((SD2SDSub (DecSD (m,1,k))),(1 + 1)) = SDSub_Add_Carry (m,k)
thus  DigA_SDSub ((SD2SDSub (DecSD (m,1,k))),(1 + 1)) = SDSub_Add_Carry ((DigA ((DecSD (m,1,k)),1)),k) by A1, Th3
.= SDSub_Add_Carry (m,k) by A2, RADIX_1:21 ; ::_thesis: verum
end;

theorem Th5: :: RADIX_4:5
for k, x, n being Nat st n >= 1 & k >= 3 & x is_represented_by n + 1,k holds
DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1)) = SDSub_Add_Carry ((DigA ((DecSD (x,n,k)),n)),k)
proof
let k, x, n be Nat; ::_thesis: ( n >= 1 & k >= 3 & x is_represented_by n + 1,k implies DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1)) = SDSub_Add_Carry ((DigA ((DecSD (x,n,k)),n)),k) )
assume that
A1: n >= 1 and
A2: k >= 3 ; ::_thesis: ( not x is_represented_by n + 1,k or DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1)) = SDSub_Add_Carry ((DigA ((DecSD (x,n,k)),n)),k) )
set xn = x mod ((Radix k) |^ n);
A3: n + 1 in Seg (n + 1) by FINSEQ_1:3;
then  DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1)) = SD2SDSubDigitS ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(n + 1),k) by RADIX_3:def_8
.= SD2SDSubDigit ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(n + 1),k) by A2, A3, RADIX_3:def_7, XXREAL_0:2
.= SDSub_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),((n + 1) -' 1))),k) by RADIX_3:def_6
.= SDSub_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(n + 0))),k) by NAT_D:34
.= SDSub_Add_Carry ((DigA ((DecSD (x,n,k)),n)),k) by A1, Lm3 ;
hence  ( not x is_represented_by n + 1,k or DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1)) = SDSub_Add_Carry ((DigA ((DecSD (x,n,k)),n)),k) ) ; ::_thesis: verum
end;

theorem Th6: :: RADIX_4:6
for k, m being Nat st 2 <= k & m is_represented_by 1,k holds
DigA_SDSub ((SD2SDSub (DecSD (m,1,k))),1) = m - ((SDSub_Add_Carry (m,k)) * (Radix k))
proof
let k, m 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
end;

theorem Th7: :: RADIX_4:7
for k, x, n being Nat st k >= 2 holds
((Radix k) |^ n) * (DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) = ((((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)))) - (((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)))
proof
let k, x, n be Nat; ::_thesis: ( k >= 2 implies ((Radix k) |^ n) * (DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) = ((((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)))) - (((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k))) )
assume A1: k >= 2 ; ::_thesis: ((Radix k) |^ n) * (DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) = ((((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)))) - (((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)))
A2: n + 1 in Seg (n + 1) by FINSEQ_1:3;
then A3: n + 1 in Seg ((n + 1) + 1) by FINSEQ_2:8;
then ((Radix k) |^ n) * (DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) = ((Radix k) |^ n) * (SD2SDSubDigitS ((DecSD (x,(n + 1),k)),(n + 1),k)) by RADIX_3:def_8
.= ((Radix k) |^ n) * (SD2SDSubDigit ((DecSD (x,(n + 1),k)),(n + 1),k)) by A1, A3, RADIX_3:def_7
.= ((Radix k) |^ n) * ((SDSub_Add_Data ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)) + (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),((n + 1) -' 1))),k))) by A2, RADIX_3:def_6
.= ((Radix k) |^ n) * ((SDSub_Add_Data ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)) + (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k))) by NAT_D:34
.= ((Radix k) |^ n) * (((DigA ((DecSD (x,(n + 1),k)),(n + 1))) - ((Radix k) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)))) + (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k))) by RADIX_3:def_4
.= ((((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)))) - ((((Radix k) |^ n) * (Radix k)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)))
.= ((((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)))) - (((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k))) by NEWTON:6 ;
hence  ((Radix k) |^ n) * (DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) = ((((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)))) - (((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k))) ; ::_thesis: verum
end;

begin

definition
let i, n, k be Nat;
let x, y be Tuple of n,k -SD_Sub ;
assume that
A1: i in Seg n and
A2: k >= 2 ;
func SDSubAddDigit (x,y,i,k) ->  Element of k -SD_Sub  equals :Def1: :: RADIX_4:def 1
(SDSub_Add_Data (((DigA_SDSub (x,i)) + (DigA_SDSub (y,i))),k)) + (SDSub_Add_Carry (((DigA_SDSub (x,(i -' 1))) + (DigA_SDSub (y,(i -' 1)))),k));
coherence
 (SDSub_Add_Data (((DigA_SDSub (x,i)) + (DigA_SDSub (y,i))),k)) + (SDSub_Add_Carry (((DigA_SDSub (x,(i -' 1))) + (DigA_SDSub (y,(i -' 1)))),k)) is Element of k -SD_Sub
proof
 DigA_SDSub (x,i) is Element of k -SD_Sub by A1, RADIX_3:18;
then A3: DigA_SDSub (x,i) in k -SD_Sub ;
set SDAC = SDSub_Add_Carry (((DigA_SDSub (x,(i -' 1))) + (DigA_SDSub (y,(i -' 1)))),k);
set SDAD = SDSub_Add_Data (((DigA_SDSub (x,i)) + (DigA_SDSub (y,i))),k);
A4: - 1 <= SDSub_Add_Carry (((DigA_SDSub (x,(i -' 1))) + (DigA_SDSub (y,(i -' 1)))),k) by RADIX_3:12;
A5: SDSub_Add_Carry (((DigA_SDSub (x,(i -' 1))) + (DigA_SDSub (y,(i -' 1)))),k) <= 1 by RADIX_3:12;
 ( k -SD_Sub c= k -SD & DigA_SDSub (y,i) is Element of k -SD_Sub ) by A1, A2, RADIX_3:4, RADIX_3:18;
then A6: SDSub_Add_Data (((DigA_SDSub (x,i)) + (DigA_SDSub (y,i))),k) in k -SD_Sub_S by A2, A3, RADIX_3:19;
then  SDSub_Add_Data (((DigA_SDSub (x,i)) + (DigA_SDSub (y,i))),k) >= - (Radix (k -' 1)) by Lm1;
then A7: (- (Radix (k -' 1))) + (- 1) <= (SDSub_Add_Data (((DigA_SDSub (x,i)) + (DigA_SDSub (y,i))),k)) + (SDSub_Add_Carry (((DigA_SDSub (x,(i -' 1))) + (DigA_SDSub (y,(i -' 1)))),k)) by A4, XREAL_1:7;
 SDSub_Add_Data (((DigA_SDSub (x,i)) + (DigA_SDSub (y,i))),k) <= (Radix (k -' 1)) - 1 by A6, Lm1;
then A8: (SDSub_Add_Data (((DigA_SDSub (x,i)) + (DigA_SDSub (y,i))),k)) + (SDSub_Add_Carry (((DigA_SDSub (x,(i -' 1))) + (DigA_SDSub (y,(i -' 1)))),k)) <= ((Radix (k -' 1)) - 1) + 1 by A5, XREAL_1:7;
 ( (SDSub_Add_Data (((DigA_SDSub (x,i)) + (DigA_SDSub (y,i))),k)) + (SDSub_Add_Carry (((DigA_SDSub (x,(i -' 1))) + (DigA_SDSub (y,(i -' 1)))),k)) is Element of INT & k -SD_Sub =  {  w where w is Element of INT : ( w >= (- (Radix (k -' 1))) - 1 & w <= Radix (k -' 1) )  }  ) by INT_1:def_2, RADIX_3:def_2;
then  (SDSub_Add_Data (((DigA_SDSub (x,i)) + (DigA_SDSub (y,i))),k)) + (SDSub_Add_Carry (((DigA_SDSub (x,(i -' 1))) + (DigA_SDSub (y,(i -' 1)))),k)) in k -SD_Sub by A7, A8;
hence  (SDSub_Add_Data (((DigA_SDSub (x,i)) + (DigA_SDSub (y,i))),k)) + (SDSub_Add_Carry (((DigA_SDSub (x,(i -' 1))) + (DigA_SDSub (y,(i -' 1)))),k)) is Element of k -SD_Sub ; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines SDSubAddDigit RADIX_4:def_1_:_
 for i, n, k being Nat
for x, y being Tuple of n,k -SD_Sub st i in Seg n & k >= 2 holds
SDSubAddDigit (x,y,i,k) = (SDSub_Add_Data (((DigA_SDSub (x,i)) + (DigA_SDSub (y,i))),k)) + (SDSub_Add_Carry (((DigA_SDSub (x,(i -' 1))) + (DigA_SDSub (y,(i -' 1)))),k));

definition
let n, k be Nat;
let x, y be Tuple of n,k -SD_Sub ;
funcx '+' y ->  Tuple of n,k -SD_Sub  means :Def2: :: RADIX_4:def 2
 for i being Nat st i in Seg n holds
DigA_SDSub (it,i) = SDSubAddDigit (x,y,i,k);
existence
 ex b1 being Tuple of n,k -SD_Sub st
for i being Nat st i in Seg n holds
DigA_SDSub (b1,i) = SDSubAddDigit (x,y,i,k)
proof
deffunc H1( Nat) ->  Element of k -SD_Sub = SDSubAddDigit (x,y,$1,k);
consider z being FinSequence of k -SD_Sub  such that
A1: len z = n and
A2: for j being Nat st j in dom z holds
z . j = H1(j) from FINSEQ_2:sch_1();
A3: dom z = Seg n by A1, FINSEQ_1:def_3;
 z is Element of n -tuples_on (k -SD_Sub) by A1, FINSEQ_2:92;
then reconsider z = z as Tuple of n,k -SD_Sub ;
take  z ; ::_thesis: for i being Nat st i in Seg n holds
DigA_SDSub (z,i) = SDSubAddDigit (x,y,i,k)
let i be Nat; ::_thesis: ( i in Seg n implies DigA_SDSub (z,i) = SDSubAddDigit (x,y,i,k) )
assume A4: i in Seg n ; ::_thesis: DigA_SDSub (z,i) = SDSubAddDigit (x,y,i,k)
hence  DigA_SDSub (z,i) = z . i by RADIX_3:def_5
.= SDSubAddDigit (x,y,i,k) by A2, A3, A4 ;
::_thesis: verum
end;
uniqueness
 for b1, b2 being Tuple of n,k -SD_Sub st ( for i being Nat st i in Seg n holds
DigA_SDSub (b1,i) = SDSubAddDigit (x,y,i,k) ) & ( for i being Nat st i in Seg n holds
DigA_SDSub (b2,i) = SDSubAddDigit (x,y,i,k) ) holds
b1 = b2
proof
let k1, k2 be Tuple of n,k -SD_Sub ; ::_thesis: ( ( for i being Nat st i in Seg n holds
DigA_SDSub (k1,i) = SDSubAddDigit (x,y,i,k) ) & ( for i being Nat st i in Seg n holds
DigA_SDSub (k2,i) = SDSubAddDigit (x,y,i,k) ) implies k1 = k2 )
assume that
A5: for i being Nat st i in Seg n holds
DigA_SDSub (k1,i) = SDSubAddDigit (x,y,i,k) and
A6: for i being Nat st i in Seg n holds
DigA_SDSub (k2,i) = SDSubAddDigit (x,y,i,k) ; ::_thesis: k1 = k2
A7: len k1 = n by CARD_1:def_7;
then A8: dom k1 = Seg n by FINSEQ_1:def_3;
A9: now__::_thesis:_for_j_being_Nat_st_j_in_dom_k1_holds_
k1_._j_=_k2_._j
let j be Nat; ::_thesis: ( j in dom k1 implies k1 . j = k2 . j )
assume A10: j in dom k1 ; ::_thesis: k1 . j = k2 . j
then k1 . j = DigA_SDSub (k1,j) by A8, RADIX_3:def_5
.= SDSubAddDigit (x,y,j,k) by A5, A8, A10
.= DigA_SDSub (k2,j) by A6, A8, A10
.= k2 . j by A8, A10, RADIX_3:def_5 ;
hence  k1 . j = k2 . j ; ::_thesis: verum
end;
 len k2 = n by CARD_1:def_7;
hence  k1 = k2 by A7, A9, FINSEQ_2:9; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines '+' RADIX_4:def_2_:_
 for n, k being Nat
for x, y, b5 being Tuple of n,k -SD_Sub holds
( b5 = x '+' y iff for i being Nat st i in Seg n holds
DigA_SDSub (b5,i) = SDSubAddDigit (x,y,i,k) );

theorem Th8: :: RADIX_4:8
for n, k, x, y, i being Nat st i in Seg n & 2 <= k holds
SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k)
proof
let n, k, x, y, i be Nat; ::_thesis: ( i in Seg n & 2 <= k implies SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k) )
set X = x mod ((Radix k) |^ n);
set Y = y mod ((Radix k) |^ n);
assume A1: i in Seg n ; ::_thesis: ( not 2 <= k or SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k) )
then  i <= n by FINSEQ_1:1;
then A2: i <= n + 1 by NAT_1:12;
A3: 1 <= i by A1, FINSEQ_1:1;
then A4: i in Seg (n + 1) by A2, FINSEQ_1:1;
 i <= (n + 1) + 1 by A2, NAT_1:12;
then A5: i in Seg ((n + 1) + 1) by A3, FINSEQ_1:1;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
assume A6: 2 <= k ; ::_thesis: SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k)
then A7: SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),i)) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),i))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(i -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(i -' 1)))),k)) by A5, Def1;
now__::_thesis:_SDSubAddDigit_((SD2SDSub_(DecSD_(x,(n_+_1),k))),(SD2SDSub_(DecSD_(y,(n_+_1),k))),i,k)_=_SDSubAddDigit_((SD2SDSub_(DecSD_((x_mod_((Radix_k)_|^_n)),n,k))),(SD2SDSub_(DecSD_((y_mod_((Radix_k)_|^_n)),n,k))),i,k)
percases ( i = 1 or i <> 1 ) ;
supposeA8: i = 1 ; ::_thesis: SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k)
then A9: DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),(i -' 1)) = DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),0) by XREAL_1:232
.= 0 by RADIX_3:def_5 ;
A10: DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(i -' 1)) = DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),0) by A8, XREAL_1:232
.= 0 by RADIX_3:def_5 ;
A11: DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(i -' 1)) = DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),0) by A8, XREAL_1:232
.= 0 by RADIX_3:def_5 ;
A12: DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(i -' 1)) = DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),0) by A8, XREAL_1:232
.= 0 by RADIX_3:def_5 ;
 ( DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),i) & DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i) ) by A1, A6, RADIX_3:20;
hence  SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k) by A4, A6, A7, A12, A11, A10, A9, Def1; ::_thesis: verum
end;
supposeA13: i <> 1 ; ::_thesis: SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k)
 i >= 1 by A1, FINSEQ_1:1;
then  1 < i by A13, XXREAL_0:1;
then A14: 0 + 1 <= i -' 1 by INT_1:7, JORDAN12:1;
 i <= n by A1, FINSEQ_1:1;
then  i -' 1 <= n by NAT_D:44;
then A15: i -' 1 in Seg n by A14, FINSEQ_1:1;
SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),i)) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),i))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(i -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(i -' 1)))),k)) by A1, A6, A7, RADIX_3:20
.= (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),i)) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(i -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(i -' 1)))),k)) by A1, A6, RADIX_3:20
.= (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),i)) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(i -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(i -' 1)))),k)) by A6, A15, RADIX_3:20
.= (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),i)) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(i -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),(i -' 1)))),k)) by A6, A15, RADIX_3:20
.= SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k) by A4, A6, Def1 ;
hence  SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k) ; ::_thesis: verum
end;
end;
end;
hence  SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k) ; ::_thesis: verum
end;

theorem :: RADIX_4:9
for n being Nat st n >= 1 holds
for k, x, y being Nat st k >= 3 & x is_represented_by n,k & y is_represented_by n,k holds
x + y = SDSub2IntOut ((SD2SDSub (DecSD (x,n,k))) '+' (SD2SDSub (DecSD (y,n,k))))
proof
defpred S1[ Nat] means  for k, x, y being Nat st k >= 3 & x is_represented_by $1,k & y is_represented_by $1,k holds
x + y = SDSub2IntOut ((SD2SDSub (DecSD (x,$1,k))) '+' (SD2SDSub (DecSD (y,$1,k))));
let n be Nat; ::_thesis: ( n >= 1 implies for k, x, y being Nat st k >= 3 & x is_represented_by n,k & y is_represented_by n,k holds
x + y = SDSub2IntOut ((SD2SDSub (DecSD (x,n,k))) '+' (SD2SDSub (DecSD (y,n,k)))) )
assume A1: n >= 1 ; ::_thesis: for k, x, y being Nat st k >= 3 & x is_represented_by n,k & y is_represented_by n,k holds
x + y = SDSub2IntOut ((SD2SDSub (DecSD (x,n,k))) '+' (SD2SDSub (DecSD (y,n,k))))
A2: for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
A3: n >= 1 and
A4: S1[n] ; ::_thesis: S1[n + 1]
let k, x, y be Nat; ::_thesis: ( k >= 3 & x is_represented_by n + 1,k & y is_represented_by n + 1,k implies x + y = SDSub2IntOut ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))) )
assume that
A5: k >= 3 and
A6: x is_represented_by n + 1,k and
A7: y is_represented_by n + 1,k ; ::_thesis: x + y = SDSub2IntOut ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k))))
reconsider k = k, x = x, y = y as Element of NAT by ORDINAL1:def_12;
A8: (n + 1) + 1 in Seg ((n + 1) + 1) by FINSEQ_1:3;
then A9: DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1)) = SD2SDSubDigitS ((DecSD (x,(n + 1),k)),((n + 1) + 1),k) by RADIX_3:def_8
.= SD2SDSubDigit ((DecSD (x,(n + 1),k)),((n + 1) + 1),k) by A5, A8, RADIX_3:def_7, XXREAL_0:2
.= SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(((n + 1) + 1) -' 1))),k) by RADIX_3:def_6
.= SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k) by NAT_D:34 ;
A10: DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),((n + 1) + 1)) = SD2SDSubDigitS ((DecSD (y,(n + 1),k)),((n + 1) + 1),k) by A8, RADIX_3:def_8
.= SD2SDSubDigit ((DecSD (y,(n + 1),k)),((n + 1) + 1),k) by A5, A8, RADIX_3:def_7, XXREAL_0:2
.= SDSub_Add_Carry ((DigA ((DecSD (y,(n + 1),k)),(((n + 1) + 1) -' 1))),k) by RADIX_3:def_6
.= SDSub_Add_Carry ((DigA ((DecSD (y,(n + 1),k)),(n + 1))),k) by NAT_D:34 ;
set yn = y mod ((Radix k) |^ n);
set xn = x mod ((Radix k) |^ n);
set zn = (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)));
deffunc H1( Nat) ->  Element of INT = SDSub2INTDigit (((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))),$1,k);
consider znpp being FinSequence of INT  such that
A11: len znpp = n and
A12: for i being Nat st i in dom znpp holds
znpp . i = H1(i) from FINSEQ_2:sch_1();
A13: len (SDSub2INT ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))))) = n + 1 by CARD_1:def_7;
A14: dom znpp = Seg n by A11, FINSEQ_1:def_3;
A15: for j being Nat st 1 <= j & j <= len (SDSub2INT ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))))) holds
(SDSub2INT ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))))) . j = (znpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))),(n + 1),k))*>) . j
proof
let j be Nat; ::_thesis: ( 1 <= j & j <= len (SDSub2INT ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))))) implies (SDSub2INT ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))))) . j = (znpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))),(n + 1),k))*>) . j )
assume  ( 1 <= j & j <= len (SDSub2INT ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))))) ) ; ::_thesis: (SDSub2INT ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))))) . j = (znpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))),(n + 1),k))*>) . j
then A16: j in Seg (n + 1) by A13, FINSEQ_1:1;
then A17: j in dom (SDSub2INT ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))))) by A13, FINSEQ_1:def_3;
now__::_thesis:_(SDSub2INT_((SD2SDSub_(DecSD_((x_mod_((Radix_k)_|^_n)),n,k)))_'+'_(SD2SDSub_(DecSD_((y_mod_((Radix_k)_|^_n)),n,k)))))_._j_=_(znpp_^_<*(SDSub2INTDigit_(((SD2SDSub_(DecSD_((x_mod_((Radix_k)_|^_n)),n,k)))_'+'_(SD2SDSub_(DecSD_((y_mod_((Radix_k)_|^_n)),n,k)))),(n_+_1),k))*>)_._j
percases ( j in Seg n or j = n + 1 ) by A16, FINSEQ_2:7;
supposeA18: j in Seg n ; ::_thesis: (SDSub2INT ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))))) . j = (znpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))),(n + 1),k))*>) . j
then  j in dom znpp by A11, FINSEQ_1:def_3;
then (znpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))),(n + 1),k))*>) . j = znpp . j by FINSEQ_1:def_7
.= SDSub2INTDigit (((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))),j,k) by A12, A14, A18
.= (SDSub2INT ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))))) /. j by A16, RADIX_3:def_11
.= (SDSub2INT ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))))) . j by A17, PARTFUN1:def_6 ;
hence  (SDSub2INT ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))))) . j = (znpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))),(n + 1),k))*>) . j ; ::_thesis: verum
end;
supposeA19: j = n + 1 ; ::_thesis: (SDSub2INT ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))))) . j = (znpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))),(n + 1),k))*>) . j
A20: j in dom (SDSub2INT ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))))) by A13, A16, FINSEQ_1:def_3;
(znpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))),(n + 1),k))*>) . j = SDSub2INTDigit (((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))),(n + 1),k) by A11, A19, FINSEQ_1:42
.= (SDSub2INT ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))))) /. (n + 1) by A16, A19, RADIX_3:def_11
.= (SDSub2INT ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))))) . j by A19, A20, PARTFUN1:def_6 ;
hence  (SDSub2INT ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))))) . j = (znpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))),(n + 1),k))*>) . j ; ::_thesis: verum
end;
end;
end;
hence  (SDSub2INT ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))))) . j = (znpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))),(n + 1),k))*>) . j ; ::_thesis: verum
end;
 len (znpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))),(n + 1),k))*>) = n + 1 by A11, FINSEQ_2:16;
then A21: SDSub2INT ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))) = znpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))),(n + 1),k))*> by A13, A15, FINSEQ_1:14;
A22: Radix k > 0 by POWER:34;
then  y mod ((Radix k) |^ n) < (Radix k) |^ n by NAT_D:1, PREPOWER:6;
then A23: y mod ((Radix k) |^ n) is_represented_by n,k by RADIX_1:def_12;
set SDN1 = (DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(n + 1)));
set z = (SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)));
deffunc H2( Nat) ->  Element of INT = SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),$1,k);
consider zpp being FinSequence of INT  such that
A24: len zpp = n and
A25: for i being Nat st i in dom zpp holds
zpp . i = H2(i) from FINSEQ_2:sch_1();
consider zp being FinSequence of INT  such that
A26: len zp = n + 1 and
A27: for i being Nat st i in dom zp holds
zp . i = H2(i) from FINSEQ_2:sch_1();
A28: dom zpp = Seg n by A24, FINSEQ_1:def_3;
 for j being Nat st 1 <= j & j <= len znpp holds
znpp . j = zpp . j
proof
let j be Nat; ::_thesis: ( 1 <= j & j <= len znpp implies znpp . j = zpp . j )
assume that
A29: 1 <= j and
A30: j <= len znpp ; ::_thesis: znpp . j = zpp . j
A31: j <= n + 1 by A11, A30, NAT_1:12;
then A32: j in Seg (n + 1) by A29, FINSEQ_1:1;
 j <= (n + 1) + 1 by A31, NAT_1:12;
then A33: j in Seg ((n + 1) + 1) by A29, FINSEQ_1:1;
A34: j in Seg n by A11, A29, A30, FINSEQ_1:1;
then zpp . j = SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),j,k) by A25, A28
.= ((Radix k) |^ (j -' 1)) * (DigB_SDSub (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),j)) by RADIX_3:def_10
.= ((Radix k) |^ (j -' 1)) * (DigA_SDSub (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),j)) by RADIX_3:def_9
.= ((Radix k) |^ (j -' 1)) * (SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),j,k)) by A33, Def2
.= ((Radix k) |^ (j -' 1)) * (SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),j,k)) by A5, A34, Th8, XXREAL_0:2
.= ((Radix k) |^ (j -' 1)) * (DigA_SDSub (((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))),j)) by A32, Def2
.= ((Radix k) |^ (j -' 1)) * (DigB_SDSub (((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))),j)) by RADIX_3:def_9
.= SDSub2INTDigit (((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))),j,k) by RADIX_3:def_10
.= znpp . j by A12, A14, A34 ;
hence  znpp . j = zpp . j ; ::_thesis: verum
end;
then A35: zpp = znpp by A24, A11, FINSEQ_1:14;
set RN1 = (Radix k) |^ (n + 1);
set SDN11 = (DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),((n + 1) + 1)));
set RN1SD11 = ((Radix k) |^ (n + 1)) * (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),((n + 1) + 1)))),k));
set RN = (Radix k) |^ n;
reconsider RNDx11 = ((Radix k) |^ n) * (DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))), RNDy11 = ((Radix k) |^ n) * (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(n + 1))), RN1Cx11 = ((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)), RN1Cy11 = ((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (y,(n + 1),k)),(n + 1))),k)), RNCx1 = ((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)), RNCy1 = ((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (y,(n + 1),k)),n)),k)), RNCx = ((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,n,k)),n)),k)), RNCy = ((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (y,n,k)),n)),k)) as Integer ;
set SDN = (DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),n)) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),n));
set RNSC = ((Radix k) |^ n) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),n)) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),n))),k));
A36: SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),((n + 1) + 1),k) = ((Radix k) |^ (((n + 1) + 1) -' 1)) * (DigB_SDSub (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),((n + 1) + 1))) by RADIX_3:def_10
.= ((Radix k) |^ (((n + 1) + 1) -' 1)) * (DigA_SDSub (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),((n + 1) + 1))) by RADIX_3:def_9
.= ((Radix k) |^ (n + 1)) * (DigA_SDSub (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),((n + 1) + 1))) by NAT_D:34
.= ((Radix k) |^ (n + 1)) * (SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),((n + 1) + 1),k)) by A8, Def2
.= ((Radix k) |^ (n + 1)) * ((SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),((n + 1) + 1)))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(((n + 1) + 1) -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(((n + 1) + 1) -' 1)))),k))) by A5, A8, Def1, XXREAL_0:2
.= ((Radix k) |^ (n + 1)) * ((SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),((n + 1) + 1)))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(((n + 1) + 1) -' 1)))),k))) by NAT_D:34
.= ((Radix k) |^ (n + 1)) * (((SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),((n + 1) + 1)))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(n + 1)))),k))) + 0) by NAT_D:34
.= (((Radix k) |^ (n + 1)) * (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),((n + 1) + 1)))),k))) + (((Radix k) |^ (n + 1)) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(n + 1)))),k))) ;
 ((Radix k) |^ (n + 1)) * (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),((n + 1) + 1)))),k)) = ((Radix k) |^ (n + 1)) * (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),((n + 1) + 1)))) - ((Radix k) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),((n + 1) + 1)))),k)))) by RADIX_3:def_4;
then A37: ((Radix k) |^ (n + 1)) * (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),((n + 1) + 1)))),k)) = ((Radix k) |^ (n + 1)) * (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),((n + 1) + 1)))) - ((Radix k) * 0)) by A5, A9, A10, Th2
.= ((Radix k) |^ (n + 1)) * ((SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)) + (SDSub_Add_Carry ((DigA ((DecSD (y,(n + 1),k)),(n + 1))),k))) by A9, A10 ;
A38: ((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1))) = ((Radix k) |^ n) * (x div ((Radix k) |^ n)) by A6, RADIX_1:24;
 x mod ((Radix k) |^ n) < (Radix k) |^ n by A22, NAT_D:1, PREPOWER:6;
then  x mod ((Radix k) |^ n) is_represented_by n,k by RADIX_1:def_12;
then (x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n)) = SDSub2IntOut ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))) by A4, A5, A23
.= Sum (SDSub2INT ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))))) by RADIX_3:def_12 ;
then A39: ((x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n))) + 0 = (Sum znpp) + (SDSub2INTDigit (((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))),(n + 1),k)) by A21, RVSUM_1:74;
set SDACy = SDSub_Add_Carry ((DigA ((DecSD (y,n,k)),n)),k);
set SDACx = SDSub_Add_Carry ((DigA ((DecSD (x,n,k)),n)),k);
A40: SDSub_Add_Data (((SDSub_Add_Carry ((DigA ((DecSD (x,n,k)),n)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (y,n,k)),n)),k))),k) = ((SDSub_Add_Carry ((DigA ((DecSD (x,n,k)),n)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (y,n,k)),n)),k))) - ((Radix k) * (SDSub_Add_Carry (((SDSub_Add_Carry ((DigA ((DecSD (x,n,k)),n)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (y,n,k)),n)),k))),k))) by RADIX_3:def_4
.= ((SDSub_Add_Carry ((DigA ((DecSD (x,n,k)),n)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (y,n,k)),n)),k))) - ((Radix k) * 0) by A5, Th2 ;
 n <> 0 by A3;
then A41: n in Seg n by FINSEQ_1:3;
A42: dom zp = Seg (n + 1) by A26, FINSEQ_1:def_3;
A43: for j being Nat st 1 <= j & j <= len zp holds
zp . j = (zpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),(n + 1),k))*>) . j
proof
let j be Nat; ::_thesis: ( 1 <= j & j <= len zp implies zp . j = (zpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),(n + 1),k))*>) . j )
assume  ( 1 <= j & j <= len zp ) ; ::_thesis: zp . j = (zpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),(n + 1),k))*>) . j
then A44: j in Seg (n + 1) by A26, FINSEQ_1:1;
now__::_thesis:_zp_._j_=_(zpp_^_<*(SDSub2INTDigit_(((SD2SDSub_(DecSD_(x,(n_+_1),k)))_'+'_(SD2SDSub_(DecSD_(y,(n_+_1),k)))),(n_+_1),k))*>)_._j
percases ( j in Seg n or j = n + 1 ) by A44, FINSEQ_2:7;
supposeA45: j in Seg n ; ::_thesis: zp . j = (zpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),(n + 1),k))*>) . j
then  j in dom zpp by A24, FINSEQ_1:def_3;
then (zpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),(n + 1),k))*>) . j = zpp . j by FINSEQ_1:def_7
.= SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),j,k) by A25, A28, A45
.= zp . j by A27, A42, A44 ;
hence  zp . j = (zpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),(n + 1),k))*>) . j ; ::_thesis: verum
end;
supposeA46: j = n + 1 ; ::_thesis: zp . j = (zpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),(n + 1),k))*>) . j
then (zpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),(n + 1),k))*>) . j = SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),(n + 1),k) by A24, FINSEQ_1:42
.= zp . j by A27, A42, A44, A46 ;
hence  zp . j = (zpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),(n + 1),k))*>) . j ; ::_thesis: verum
end;
end;
end;
hence  zp . j = (zpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),(n + 1),k))*>) . j ; ::_thesis: verum
end;
A47: len (SDSub2INT ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k))))) = (n + 1) + 1 by CARD_1:def_7;
A48: for j being Nat st 1 <= j & j <= len (SDSub2INT ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k))))) holds
(SDSub2INT ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k))))) . j = (zp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),((n + 1) + 1),k))*>) . j
proof
let j be Nat; ::_thesis: ( 1 <= j & j <= len (SDSub2INT ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k))))) implies (SDSub2INT ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k))))) . j = (zp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),((n + 1) + 1),k))*>) . j )
assume  ( 1 <= j & j <= len (SDSub2INT ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k))))) ) ; ::_thesis: (SDSub2INT ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k))))) . j = (zp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),((n + 1) + 1),k))*>) . j
then A49: j in Seg ((n + 1) + 1) by A47, FINSEQ_1:1;
then A50: j in dom (SDSub2INT ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k))))) by A47, FINSEQ_1:def_3;
now__::_thesis:_(SDSub2INT_((SD2SDSub_(DecSD_(x,(n_+_1),k)))_'+'_(SD2SDSub_(DecSD_(y,(n_+_1),k)))))_._j_=_(zp_^_<*(SDSub2INTDigit_(((SD2SDSub_(DecSD_(x,(n_+_1),k)))_'+'_(SD2SDSub_(DecSD_(y,(n_+_1),k)))),((n_+_1)_+_1),k))*>)_._j
percases ( j in Seg (n + 1) or j = (n + 1) + 1 ) by A49, FINSEQ_2:7;
supposeA51: j in Seg (n + 1) ; ::_thesis: (SDSub2INT ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k))))) . j = (zp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),((n + 1) + 1),k))*>) . j
then  j in dom zp by A26, FINSEQ_1:def_3;
then (zp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),((n + 1) + 1),k))*>) . j = zp . j by FINSEQ_1:def_7
.= SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),j,k) by A27, A42, A51
.= (SDSub2INT ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k))))) /. j by A49, RADIX_3:def_11
.= (SDSub2INT ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k))))) . j by A50, PARTFUN1:def_6 ;
hence  (SDSub2INT ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k))))) . j = (zp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),((n + 1) + 1),k))*>) . j ; ::_thesis: verum
end;
supposeA52: j = (n + 1) + 1 ; ::_thesis: (SDSub2INT ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k))))) . j = (zp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),((n + 1) + 1),k))*>) . j
A53: j in dom (SDSub2INT ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k))))) by A47, A49, FINSEQ_1:def_3;
(zp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),((n + 1) + 1),k))*>) . j = SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),((n + 1) + 1),k) by A26, A52, FINSEQ_1:42
.= (SDSub2INT ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k))))) /. ((n + 1) + 1) by A49, A52, RADIX_3:def_11
.= (SDSub2INT ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k))))) . j by A52, A53, PARTFUN1:def_6 ;
hence  (SDSub2INT ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k))))) . j = (zp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),((n + 1) + 1),k))*>) . j ; ::_thesis: verum
end;
end;
end;
hence  (SDSub2INT ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k))))) . j = (zp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),((n + 1) + 1),k))*>) . j ; ::_thesis: verum
end;
 len (zpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),(n + 1),k))*>) = n + 1 by A24, FINSEQ_2:16;
then A54: zp = zpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),(n + 1),k))*> by A26, A43, FINSEQ_1:14;
 len (zp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),((n + 1) + 1),k))*>) = (n + 1) + 1 by A26, FINSEQ_2:16;
then  SDSub2INT ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))) = zp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),((n + 1) + 1),k))*> by A47, A48, FINSEQ_1:14;
then A55: Sum (SDSub2INT ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k))))) = (Sum zp) + (SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),((n + 1) + 1),k)) by RVSUM_1:74
.= ((Sum znpp) + (SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),(n + 1),k))) + (SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),((n + 1) + 1),k)) by A54, A35, RVSUM_1:74 ;
A56: n + 1 in Seg (n + 1) by FINSEQ_1:3;
then A57: n + 1 in Seg ((n + 1) + 1) by FINSEQ_2:8;
SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),(n + 1),k) = ((Radix k) |^ ((n + 1) -' 1)) * (DigB_SDSub (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),(n + 1))) by RADIX_3:def_10
.= ((Radix k) |^ ((n + 1) -' 1)) * (DigA_SDSub (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),(n + 1))) by RADIX_3:def_9
.= ((Radix k) |^ n) * (DigA_SDSub (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),(n + 1))) by NAT_D:34
.= ((Radix k) |^ n) * (SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),(n + 1),k)) by A57, Def2
.= ((Radix k) |^ n) * ((SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(n + 1)))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),((n + 1) -' 1)))),k))) by A5, A57, Def1, XXREAL_0:2
.= ((Radix k) |^ n) * ((SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(n + 1)))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),n)) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),((n + 1) -' 1)))),k))) by NAT_D:34
.= ((Radix k) |^ n) * (((SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(n + 1)))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),n)) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),n))),k))) + 0) by NAT_D:34
.= (((Radix k) |^ n) * (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(n + 1)))),k))) + (((Radix k) |^ n) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),n)) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),n))),k)))
.= (((Radix k) |^ n) * (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(n + 1)))) - ((Radix k) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(n + 1)))),k))))) + (((Radix k) |^ n) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),n)) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),n))),k))) by RADIX_3:def_4
.= ((((Radix k) |^ n) * ((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(n + 1))))) - ((((Radix k) |^ n) * (Radix k)) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(n + 1)))),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),n)) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),n))),k)))
.= ((((Radix k) |^ n) * ((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(n + 1))))) - (((Radix k) |^ (n + 1)) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(n + 1)))),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),n)) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),n))),k))) by NEWTON:6
.= ((((Radix k) |^ n) * ((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(n + 1))))) + (- (((Radix k) |^ (n + 1)) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(n + 1)))),k))))) + (((Radix k) |^ n) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),n)) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),n))),k))) ;
then A58: Sum (SDSub2INT ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k))))) = ((((x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n))) + (((Radix k) |^ n) * ((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(n + 1)))))) + ((- (SDSub2INTDigit (((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))),(n + 1),k))) + (((Radix k) |^ n) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),n)) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),n))),k))))) + (((Radix k) |^ (n + 1)) * (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),((n + 1) + 1)))),k))) by A55, A39, A36;
SDSub2INTDigit (((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))),(n + 1),k) = ((Radix k) |^ ((n + 1) -' 1)) * (DigB_SDSub (((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))),(n + 1))) by RADIX_3:def_10
.= ((Radix k) |^ ((n + 1) -' 1)) * (DigA_SDSub (((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))),(n + 1))) by RADIX_3:def_9
.= ((Radix k) |^ n) * (DigA_SDSub (((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) '+' (SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))),(n + 1))) by NAT_D:34
.= ((Radix k) |^ n) * (SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),(n + 1),k)) by A56, Def2
.= ((Radix k) |^ n) * ((SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1))) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),(n + 1)))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),((n + 1) -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),((n + 1) -' 1)))),k))) by A56, A5, Def1, XXREAL_0:2
.= ((Radix k) |^ n) * ((SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1))) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),(n + 1)))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),n)) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),((n + 1) -' 1)))),k))) by NAT_D:34
.= ((Radix k) |^ n) * ((SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1))) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),(n + 1)))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),n)) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),n))),k))) by NAT_D:34
.= ((Radix k) |^ n) * ((SDSub_Add_Data (((SDSub_Add_Carry ((DigA ((DecSD (x,n,k)),n)),k)) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),(n + 1)))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),n)) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),n))),k))) by A3, A5, A6, Th5
.= ((Radix k) |^ n) * ((SDSub_Add_Data (((SDSub_Add_Carry ((DigA ((DecSD (x,n,k)),n)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (y,n,k)),n)),k))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),n)) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),n))),k))) by A3, A5, A7, Th5
.= ((Radix k) |^ n) * ((SDSub_Add_Data (((SDSub_Add_Carry ((DigA ((DecSD (x,n,k)),n)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (y,n,k)),n)),k))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),n)) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),n))),k))) by A41, A5, RADIX_3:20, XXREAL_0:2
.= ((Radix k) |^ n) * ((SDSub_Add_Data (((SDSub_Add_Carry ((DigA ((DecSD (x,n,k)),n)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (y,n,k)),n)),k))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),n)) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),n))),k))) by A41, A5, RADIX_3:20, XXREAL_0:2
.= (((Radix k) |^ n) * (SDSub_Add_Data (((SDSub_Add_Carry ((DigA ((DecSD (x,n,k)),n)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (y,n,k)),n)),k))),k))) + (((Radix k) |^ n) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),n)) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),n))),k))) ;
then A59: Sum (SDSub2INT ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k))))) = (((((x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n))) + RNDx11) + RNDy11) + (- (RNCx + RNCy))) + (RN1Cx11 + RN1Cy11) by A40, A58, A37
.= (((((x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n))) + (((((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)))) - RN1Cx11) + RNCx1)) + RNDy11) + (- (RNCx + RNCy))) + (RN1Cx11 + RN1Cy11) by A5, Th7, XXREAL_0:2
.= ((((((x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n))) + (((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1))))) + RNCx1) + RNDy11) + RN1Cy11) - (RNCx + RNCy)
.= ((((((x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n))) + (((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1))))) + RNCx1) + (((((Radix k) |^ n) * (DigA ((DecSD (y,(n + 1),k)),(n + 1)))) - RN1Cy11) + RNCy1)) + RN1Cy11) - (RNCx + RNCy) by A5, Th7, XXREAL_0:2
.= ((((((((x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n))) + (((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1))))) + RNCx1) + (((Radix k) |^ n) * (DigA ((DecSD (y,(n + 1),k)),(n + 1))))) + (- RN1Cy11)) + RNCy1) + RN1Cy11) + (- (RNCx + RNCy))
.= ((((((x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n))) + (((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1))))) + RNCx1) + (((Radix k) |^ n) * (DigA ((DecSD (y,(n + 1),k)),(n + 1))))) + RNCy1) + (- (RNCx1 + RNCy)) by A41, Lm2
.= ((((((x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n))) + (((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1))))) + RNCx1) + (((Radix k) |^ n) * (DigA ((DecSD (y,(n + 1),k)),(n + 1))))) + RNCy1) + (- (RNCx1 + RNCy1)) by A41, Lm2
.= ((((x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n))) + (((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1))))) + 0) + (((Radix k) |^ n) * (DigA ((DecSD (y,(n + 1),k)),(n + 1)))) ;
A60: y = ((y div ((Radix k) |^ n)) * ((Radix k) |^ n)) + (y mod ((Radix k) |^ n)) by A22, NAT_D:2, PREPOWER:6;
 x = ((x div ((Radix k) |^ n)) * ((Radix k) |^ n)) + (x mod ((Radix k) |^ n)) by A22, NAT_D:2, PREPOWER:6;
then  Sum (SDSub2INT ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k))))) = ((y mod ((Radix k) |^ n)) + x) + (((Radix k) |^ n) * (y div ((Radix k) |^ n))) by A7, A59, A38, RADIX_1:24;
hence  x + y = SDSub2IntOut ((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))) by A60, RADIX_3:def_12; ::_thesis: verum
end;
A61: S1[1]
proof
let k, x, y be Nat; ::_thesis: ( k >= 3 & x is_represented_by 1,k & y is_represented_by 1,k implies x + y = SDSub2IntOut ((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k)))) )
assume that
A62: k >= 3 and
A63: x is_represented_by 1,k and
A64: y is_represented_by 1,k ; ::_thesis: x + y = SDSub2IntOut ((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k))))
reconsider k = k, x = x, y = y as Element of NAT by ORDINAL1:def_12;
set X = SD2SDSub (DecSD (x,1,k));
set Y = SD2SDSub (DecSD (y,1,k));
reconsider CRY1 = SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),1))),k) as Integer ;
reconsider DIG1 = DigA_SDSub (((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k)))),1) as Element of INT by INT_1:def_2;
reconsider RSDCX = (Radix k) * (SDSub_Add_Carry (x,k)), RSDCY = (Radix k) * (SDSub_Add_Carry (y,k)) as Integer ;
reconsider RCRY1 = (Radix k) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),1))),k)) as Integer ;
A65: 1 in Seg (1 + 1) by FINSEQ_1:1;
then A66: (SDSub2INT ((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k))))) /. 1 = SDSub2INTDigit (((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k)))),1,k) by RADIX_3:def_11
.= ((Radix k) |^ (1 -' 1)) * (DigB_SDSub (((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k)))),1)) by RADIX_3:def_10
.= ((Radix k) |^ 0) * (DigB_SDSub (((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k)))),1)) by XREAL_1:232
.= 1 * (DigB_SDSub (((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k)))),1)) by NEWTON:4
.= DigA_SDSub (((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k)))),1) by RADIX_3:def_9 ;
A67: len (SDSub2INT ((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k))))) = 1 + 1 by CARD_1:def_7;
then  1 in dom (SDSub2INT ((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k))))) by A65, FINSEQ_1:def_3;
then A68: (SDSub2INT ((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k))))) . 1 = DIG1 by A66, PARTFUN1:def_6;
 2 - 1 = 1 ;
then A69: 2 -' 1 = 1 by XREAL_0:def_2;
DigA_SDSub (((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k)))),1) = SDSubAddDigit ((SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k))),1,k) by A65, Def2
.= (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),1))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),(1 -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),(1 -' 1)))),k)) by A62, A65, Def1, XXREAL_0:2
.= (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),1))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),0)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),(1 -' 1)))),k)) by XREAL_1:232
.= (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),1))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),0)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),0))),k)) by XREAL_1:232
.= (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),1))),k)) + (SDSub_Add_Carry ((0 + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),0))),k)) by RADIX_3:def_5
.= (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),1))),k)) + (SDSub_Add_Carry ((0 + 0),k)) by RADIX_3:def_5
.= (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),1))),k)) + 0 by RADIX_3:16
.= ((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),1))) - ((Radix k) * CRY1) by RADIX_3:def_4 ;
then A70: DIG1 = ((x - RSDCX) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),1))) - RCRY1 by A62, A63, Th6, XXREAL_0:2
.= ((x - RSDCX) + (y - RSDCY)) - RCRY1 by A62, A64, Th6, XXREAL_0:2
.= (((x + y) - RSDCX) - RSDCY) - RCRY1 ;
reconsider DIG2 = (Radix k) * (DigA_SDSub (((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k)))),2)) as Element of INT by INT_1:def_2;
A71: 2 in Seg (1 + 1) by FINSEQ_1:1;
then A72: (SDSub2INT ((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k))))) /. 2 = SDSub2INTDigit (((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k)))),2,k) by RADIX_3:def_11
.= ((Radix k) |^ (2 -' 1)) * (DigB_SDSub (((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k)))),2)) by RADIX_3:def_10
.= (Radix k) * (DigB_SDSub (((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k)))),2)) by A69, NEWTON:5
.= (Radix k) * (DigA_SDSub (((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k)))),2)) by RADIX_3:def_9 ;
 2 in dom (SDSub2INT ((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k))))) by A71, A67, FINSEQ_1:def_3;
then  (SDSub2INT ((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k))))) . 2 = DIG2 by A72, PARTFUN1:def_6;
then  SDSub2INT ((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k)))) = <*DIG1,DIG2*> by A67, A68, FINSEQ_1:44;
then A73: Sum (SDSub2INT ((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k))))) = DIG1 + DIG2 by RVSUM_1:77;
DigA_SDSub (((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k)))),2) = SDSubAddDigit ((SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k))),2,k) by A71, Def2
.= (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),2)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),2))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),(2 -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),(2 -' 1)))),k)) by A62, A71, Def1, XXREAL_0:2
.= (SDSub_Add_Data (((SDSub_Add_Carry (x,k)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),2))),k)) + CRY1 by A62, A63, A69, Th4, XXREAL_0:2
.= (SDSub_Add_Data (((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))),k)) + CRY1 by A62, A64, Th4, XXREAL_0:2
.= (((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))) - ((Radix k) * (SDSub_Add_Carry (((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))),k)))) + CRY1 by RADIX_3:def_4
.= (((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))) - ((Radix k) * 0)) + CRY1 by A62, Th2
.= (((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))) - 0) + CRY1 ;
hence  x + y = SDSub2IntOut ((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k)))) by A73, A70, RADIX_3:def_12; ::_thesis: verum
end;
 for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch_8(A61, A2);
hence  for k, x, y being Nat st k >= 3 & x is_represented_by n,k & y is_represented_by n,k holds
x + y = SDSub2IntOut ((SD2SDSub (DecSD (x,n,k))) '+' (SD2SDSub (DecSD (y,n,k)))) by A1; ::_thesis: verum
end;