defpred S1[ Nat] means for k being Nat st k >= 2 holds
for tx, ty, tz, tw being Tuple of $1,k -SD st ( for i being Nat holds
( not i in Seg $1 or ( DigA (tx,i) = DigA (tz,i) & DigA (ty,i) = DigA (tw,i) ) or ( DigA (ty,i) = DigA (tz,i) & DigA (tx,i) = DigA (tw,i) ) ) ) holds
(SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty);
A1: 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
n >= 1 and
A2: S1[n] ; :: thesis: S1[n + 1]
let k be Nat; :: thesis: ( k >= 2 implies for tx, ty, tz, tw being Tuple of n + 1,k -SD st ( for i being Nat holds
( not i in Seg (n + 1) or ( DigA (tx,i) = DigA (tz,i) & DigA (ty,i) = DigA (tw,i) ) or ( DigA (ty,i) = DigA (tz,i) & DigA (tx,i) = DigA (tw,i) ) ) ) holds
(SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) )
assume A3: k >= 2 ; :: thesis: for tx, ty, tz, tw being Tuple of n + 1,k -SD st ( for i being Nat holds
( not i in Seg (n + 1) or ( DigA (tx,i) = DigA (tz,i) & DigA (ty,i) = DigA (tw,i) ) or ( DigA (ty,i) = DigA (tz,i) & DigA (tx,i) = DigA (tw,i) ) ) ) holds
(SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty)
let tx, ty, tz, tw be Tuple of n + 1,k -SD ; :: thesis: ( ( for i being Nat holds
( not i in Seg (n + 1) or ( DigA (tx,i) = DigA (tz,i) & DigA (ty,i) = DigA (tw,i) ) or ( DigA (ty,i) = DigA (tz,i) & DigA (tx,i) = DigA (tw,i) ) ) ) implies (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) )
assume A4: for i being Nat holds
( not i in Seg (n + 1) or ( DigA (tx,i) = DigA (tz,i) & DigA (ty,i) = DigA (tw,i) ) or ( DigA (ty,i) = DigA (tz,i) & DigA (tx,i) = DigA (tw,i) ) ) ; :: thesis: (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty)
deffunc H1( Nat) -> Element of INT = DigB (tx,$1);
consider txn being FinSequence of INT such that
A5: len txn = n and
A6: for i being Nat st i in dom txn holds
txn . i = H1(i) from FINSEQ_2:sch 1();
 A7: dom txn = Seg n by A5, FINSEQ_1:def 3;
rng txn c= k -SD
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng txn or z in k -SD )
assume z in rng txn ; :: thesis: z in k -SD
then consider xx being object such that
A8: xx in dom txn and
A9: z = txn . xx by FUNCT_1:def 3;
reconsider xx = xx as Element of NAT by A8;
dom txn = Seg n by A5, FINSEQ_1:def 3;
then xx in Seg (n + 1) by A8, FINSEQ_2:8;
then A10: DigA (tx,xx) is Element of k -SD by RADIX_1:16;
z = DigB (tx,xx) by A6, A8, A9
.= DigA (tx,xx) by RADIX_1:def 4 ;
hence z in k -SD by A10; :: thesis: verum
end;
then reconsider txn = txn as FinSequence of k -SD by FINSEQ_1:def 4;
A11: for i being Nat st i in Seg n holds
txn . i = tx . i
proof
let i be Nat; :: thesis: ( i in Seg n implies txn . i = tx . i )
assume A12: i in Seg n ; :: thesis: txn . i = tx . i
then A13: i in Seg (n + 1) by FINSEQ_2:8;
txn . i = DigB (tx,i) by A6, A7, A12
.= DigA (tx,i) by RADIX_1:def 4 ;
hence txn . i = tx . i by A13, RADIX_1:def 3; :: thesis: verum
end;
deffunc H2( Nat) -> Element of INT = DigB (ty,$1);
consider tyn being FinSequence of INT such that
A14: len tyn = n and
A15: for i being Nat st i in dom tyn holds
tyn . i = H2(i) from FINSEQ_2:sch 1();
 A16: dom tyn = Seg n by A14, FINSEQ_1:def 3;
rng tyn c= k -SD
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng tyn or z in k -SD )
assume z in rng tyn ; :: thesis: z in k -SD
then consider yy being object such that
A17: yy in dom tyn and
A18: z = tyn . yy by FUNCT_1:def 3;
reconsider yy = yy as Element of NAT by A17;
dom tyn = Seg n by A14, FINSEQ_1:def 3;
then yy in Seg (n + 1) by A17, FINSEQ_2:8;
then A19: DigA (ty,yy) is Element of k -SD by RADIX_1:16;
z = DigB (ty,yy) by A15, A17, A18
.= DigA (ty,yy) by RADIX_1:def 4 ;
hence z in k -SD by A19; :: thesis: verum
end;
then reconsider tyn = tyn as FinSequence of k -SD by FINSEQ_1:def 4;
A20: for i being Nat st i in Seg n holds
tyn . i = ty . i
proof
let i be Nat; :: thesis: ( i in Seg n implies tyn . i = ty . i )
assume A21: i in Seg n ; :: thesis: tyn . i = ty . i
then A22: i in Seg (n + 1) by FINSEQ_2:8;
tyn . i = DigB (ty,i) by A15, A16, A21
.= DigA (ty,i) by RADIX_1:def 4 ;
hence tyn . i = ty . i by A22, RADIX_1:def 3; :: thesis: verum
end;
deffunc H3( Nat) -> Element of INT = DigB (tz,$1);
consider tzn being FinSequence of INT such that
A23: len tzn = n and
A24: for i being Nat st i in dom tzn holds
tzn . i = H3(i) from FINSEQ_2:sch 1();
 A25: dom tzn = Seg n by A23, FINSEQ_1:def 3;
rng tzn c= k -SD
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng tzn or z in k -SD )
assume z in rng tzn ; :: thesis: z in k -SD
then consider zz being object such that
A26: zz in dom tzn and
A27: z = tzn . zz by FUNCT_1:def 3;
reconsider zz = zz as Element of NAT by A26;
dom tzn = Seg n by A23, FINSEQ_1:def 3;
then zz in Seg (n + 1) by A26, FINSEQ_2:8;
then A28: DigA (tz,zz) is Element of k -SD by RADIX_1:16;
z = DigB (tz,zz) by A24, A26, A27
.= DigA (tz,zz) by RADIX_1:def 4 ;
hence z in k -SD by A28; :: thesis: verum
end;
then reconsider tzn = tzn as FinSequence of k -SD by FINSEQ_1:def 4;
A29: for i being Nat st i in Seg n holds
tzn . i = tz . i
proof
let i be Nat; :: thesis: ( i in Seg n implies tzn . i = tz . i )
assume A30: i in Seg n ; :: thesis: tzn . i = tz . i
then A31: i in Seg (n + 1) by FINSEQ_2:8;
tzn . i = DigB (tz,i) by A24, A25, A30
.= DigA (tz,i) by RADIX_1:def 4 ;
hence tzn . i = tz . i by A31, RADIX_1:def 3; :: thesis: verum
end;
deffunc H4( Nat) -> Element of INT = DigB (tw,$1);
consider twn being FinSequence of INT such that
A32: len twn = n and
A33: for i being Nat st i in dom twn holds
twn . i = H4(i) from FINSEQ_2:sch 1();
 A34: dom twn = Seg n by A32, FINSEQ_1:def 3;
rng twn c= k -SD
proof
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in rng twn or w in k -SD )
assume w in rng twn ; :: thesis: w in k -SD
then consider ww being object such that
A35: ww in dom twn and
A36: w = twn . ww by FUNCT_1:def 3;
reconsider ww = ww as Element of NAT by A35;
dom twn = Seg n by A32, FINSEQ_1:def 3;
then ww in Seg (n + 1) by A35, FINSEQ_2:8;
then A37: DigA (tw,ww) is Element of k -SD by RADIX_1:16;
w = DigB (tw,ww) by A33, A35, A36
.= DigA (tw,ww) by RADIX_1:def 4 ;
hence w in k -SD by A37; :: thesis: verum
end;
then reconsider twn = twn as FinSequence of k -SD by FINSEQ_1:def 4;
A38: for i being Nat st i in Seg n holds
twn . i = tw . i
proof
let i be Nat; :: thesis: ( i in Seg n implies twn . i = tw . i )
assume A39: i in Seg n ; :: thesis: twn . i = tw . i
then A40: i in Seg (n + 1) by FINSEQ_2:8;
twn . i = DigB (tw,i) by A33, A34, A39
.= DigA (tw,i) by RADIX_1:def 4 ;
hence twn . i = tw . i by A40, RADIX_1:def 3; :: thesis: verum
end;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
twn is Element of n -tuples_on (k -SD) by A32, FINSEQ_2:92;
then reconsider twn = twn as Tuple of n,k -SD ;
tzn is Element of n -tuples_on (k -SD) by A23, FINSEQ_2:92;
then reconsider tzn = tzn as Tuple of n,k -SD ;
tyn is Element of n -tuples_on (k -SD) by A14, FINSEQ_2:92;
then reconsider tyn = tyn as Tuple of n,k -SD ;
A41: (SDDec tyn) + (((Radix k) |^ n) * (DigA (ty,(n + 1)))) = SDDec ty by A20, RADIX_2:10;
n + 1 in Seg (n + 1) by FINSEQ_1:3;
then A42: ( ( DigA (tx,(n + 1)) = DigA (tz,(n + 1)) & DigA (ty,(n + 1)) = DigA (tw,(n + 1)) ) or ( DigA (ty,(n + 1)) = DigA (tz,(n + 1)) & DigA (tx,(n + 1)) = DigA (tw,(n + 1)) ) ) by A4;
A43: (SDDec twn) + (((Radix k) |^ n) * (DigA (tw,(n + 1)))) = SDDec tw by A38, RADIX_2:10;
A44: (SDDec tzn) + (((Radix k) |^ n) * (DigA (tz,(n + 1)))) = SDDec tz by A29, RADIX_2:10;
txn is Element of n -tuples_on (k -SD) by A5, FINSEQ_2:92;
then reconsider txn = txn as Tuple of n,k -SD ;
for i being Nat holds
( not i in Seg n or ( DigA (txn,i) = DigA (tzn,i) & DigA (tyn,i) = DigA (twn,i) ) or ( DigA (tyn,i) = DigA (tzn,i) & DigA (txn,i) = DigA (twn,i) ) )
proof
let i be Nat; :: thesis: ( not i in Seg n or ( DigA (txn,i) = DigA (tzn,i) & DigA (tyn,i) = DigA (twn,i) ) or ( DigA (tyn,i) = DigA (tzn,i) & DigA (txn,i) = DigA (twn,i) ) )
assume A45: i in Seg n ; :: thesis: ( ( DigA (txn,i) = DigA (tzn,i) & DigA (tyn,i) = DigA (twn,i) ) or ( DigA (tyn,i) = DigA (tzn,i) & DigA (txn,i) = DigA (twn,i) ) )
then i <= n by FINSEQ_1:1;
then A46: i <= n + 1 by NAT_1:12;
1 <= i by A45, FINSEQ_1:1;
then A47: i in Seg (n + 1) by A46, FINSEQ_1:1;
then A48: DigA (ty,i) = ty . i by RADIX_1:def 3
.= tyn . i by A20, A45
.= DigA (tyn,i) by A45, RADIX_1:def 3 ;
A49: DigA (tw,i) = tw . i by A47, RADIX_1:def 3
.= twn . i by A38, A45
.= DigA (twn,i) by A45, RADIX_1:def 3 ;
A50: DigA (tz,i) = tz . i by A47, RADIX_1:def 3
.= tzn . i by A29, A45
.= DigA (tzn,i) by A45, RADIX_1:def 3 ;
DigA (tx,i) = tx . i by A47, RADIX_1:def 3
.= txn . i by A11, A45
.= DigA (txn,i) by A45, RADIX_1:def 3 ;
hence ( ( DigA (txn,i) = DigA (tzn,i) & DigA (tyn,i) = DigA (twn,i) ) or ( DigA (tyn,i) = DigA (tzn,i) & DigA (txn,i) = DigA (twn,i) ) ) by A4, A47, A48, A50, A49; :: thesis: verum
end;
then A51: (SDDec tzn) + (SDDec twn) = (SDDec txn) + (SDDec tyn) by A2, A3;
(SDDec txn) + (((Radix k) |^ n) * (DigA (tx,(n + 1)))) = SDDec tx by A11, RADIX_2:10;
hence (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) by A41, A44, A43, A51, A42; :: thesis: verum
end;
A52: S1[1]
proof
let k be Nat; :: thesis: ( k >= 2 implies for tx, ty, tz, tw being Tuple of 1,k -SD st ( for i being Nat holds
( not i in Seg 1 or ( DigA (tx,i) = DigA (tz,i) & DigA (ty,i) = DigA (tw,i) ) or ( DigA (ty,i) = DigA (tz,i) & DigA (tx,i) = DigA (tw,i) ) ) ) holds
(SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) )
assume A53: k >= 2 ; :: thesis: for tx, ty, tz, tw being Tuple of 1,k -SD st ( for i being Nat holds
( not i in Seg 1 or ( DigA (tx,i) = DigA (tz,i) & DigA (ty,i) = DigA (tw,i) ) or ( DigA (ty,i) = DigA (tz,i) & DigA (tx,i) = DigA (tw,i) ) ) ) holds
(SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty)
let tx, ty, tz, tw be Tuple of 1,k -SD ; :: thesis: ( ( for i being Nat holds
( not i in Seg 1 or ( DigA (tx,i) = DigA (tz,i) & DigA (ty,i) = DigA (tw,i) ) or ( DigA (ty,i) = DigA (tz,i) & DigA (tx,i) = DigA (tw,i) ) ) ) implies (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) )
A54: 1 in Seg 1 by FINSEQ_1:1;
A55: SDDec (tx '+' ty) = DigA ((tx '+' ty),1) by Th4
.= Add (tx,ty,1,k) by A54, RADIX_1:def 14
.= (SD_Add_Data (((DigA (tx,1)) + (DigA (ty,1))),k)) + (SD_Add_Carry ((DigA (tx,(1 -' 1))) + (DigA (ty,(1 -' 1))))) by A53, A54, RADIX_1:def 13
.= (SD_Add_Data (((DigA (tx,1)) + (DigA (ty,1))),k)) + (SD_Add_Carry ((DigA (tx,0)) + (DigA (ty,(1 -' 1))))) by XREAL_1:232
.= (SD_Add_Data (((DigA (tx,1)) + (DigA (ty,1))),k)) + (SD_Add_Carry ((DigA (tx,0)) + (DigA (ty,0)))) by XREAL_1:232
.= (SD_Add_Data (((DigA (tx,1)) + (DigA (ty,1))),k)) + (SD_Add_Carry ((DigA (tx,0)) + 0)) by RADIX_1:def 3
.= (SD_Add_Data (((DigA (tx,1)) + (DigA (ty,1))),k)) + (SD_Add_Carry (0 + 0)) by RADIX_1:def 3
.= (SD_Add_Data (((DigA (tx,1)) + (DigA (ty,1))),k)) + 0 by RADIX_1:def 10 ;
A56: SDDec (tz '+' tw) = DigA ((tz '+' tw),1) by Th4
.= Add (tz,tw,1,k) by A54, RADIX_1:def 14
.= (SD_Add_Data (((DigA (tz,1)) + (DigA (tw,1))),k)) + (SD_Add_Carry ((DigA (tz,(1 -' 1))) + (DigA (tw,(1 -' 1))))) by A53, A54, RADIX_1:def 13
.= (SD_Add_Data (((DigA (tz,1)) + (DigA (tw,1))),k)) + (SD_Add_Carry ((DigA (tz,0)) + (DigA (tw,(1 -' 1))))) by XREAL_1:232
.= (SD_Add_Data (((DigA (tz,1)) + (DigA (tw,1))),k)) + (SD_Add_Carry ((DigA (tz,0)) + (DigA (tw,0)))) by XREAL_1:232
.= (SD_Add_Data (((DigA (tz,1)) + (DigA (tw,1))),k)) + (SD_Add_Carry ((DigA (tz,0)) + 0)) by RADIX_1:def 3
.= (SD_Add_Data (((DigA (tz,1)) + (DigA (tw,1))),k)) + (SD_Add_Carry (0 + 0)) by RADIX_1:def 3
.= (SD_Add_Data (((DigA (tz,1)) + (DigA (tw,1))),k)) + 0 by RADIX_1:def 10 ;
A57: ( DigA (tx,1) = DigA (tz,1) & DigA (ty,1) = DigA (tw,1) implies (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) )
proof
assume ( DigA (tx,1) = DigA (tz,1) & DigA (ty,1) = DigA (tw,1) ) ; :: thesis: (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty)
then (SDDec tz) + (SDDec tw) = (SDDec (tx '+' ty)) + ((SD_Add_Carry ((DigA (tx,1)) + (DigA (ty,1)))) * ((Radix k) |^ 1)) by A53, A56, A55, RADIX_2:11;
hence (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) by A53, RADIX_2:11; :: thesis: verum
end;
assume A58: for j being Nat holds
( not j in Seg 1 or ( DigA (tx,j) = DigA (tz,j) & DigA (ty,j) = DigA (tw,j) ) or ( DigA (ty,j) = DigA (tz,j) & DigA (tx,j) = DigA (tw,j) ) ) ; :: thesis: (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty)
then A59: ( ( DigA (tx,1) = DigA (tz,1) & DigA (ty,1) = DigA (tw,1) ) or ( DigA (ty,1) = DigA (tz,1) & DigA (tx,1) = DigA (tw,1) ) ) by A54;
( DigA (ty,1) = DigA (tz,1) & DigA (tx,1) = DigA (tw,1) implies (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) )
proof
assume that
DigA (ty,1) = DigA (tz,1) and
DigA (tx,1) = DigA (tw,1) ; :: thesis: (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty)
(SDDec tz) + (SDDec tw) = (SDDec (tx '+' ty)) + ((SD_Add_Carry ((DigA (tx,1)) + (DigA (ty,1)))) * ((Radix k) |^ 1)) by A53, A56, A55, A59, RADIX_2:11;
hence (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) by A53, RADIX_2:11; :: thesis: verum
end;
hence (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) by A58, A54, A57; :: thesis: verum
end;
for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch 8(A52, A1);
 hence for n being Nat st n >= 1 holds
for k being Nat st k >= 2 holds
for tx, ty, tz, tw being Tuple of n,k -SD st ( for i being Nat holds
( not i in Seg n or ( DigA (tx,i) = DigA (tz,i) & DigA (ty,i) = DigA (tw,i) ) or ( DigA (ty,i) = DigA (tz,i) & DigA (tx,i) = DigA (tw,i) ) ) ) holds
(SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) ; :: thesis: verum