defpred S₁[ 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 & S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( n >= 1 & S₁[n] implies S₁[n + 1] )
assume that
n >= 1 and
A2: S₁[n] ; :: thesis: S₁[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 H₁( Nat) -> Element of K455() = 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 = H₁(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 set ; :: 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 set such that
A8: xx in dom txn and
A9: z = txn . xx by FUNCT_1:def 5;
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:9;
then A10: DigA tx,xx is Element of k -SD by RADIX_1:19;
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:9;
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 H₂( Nat) -> Element of K455() = 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 = H₂(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 set ; :: 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 set such that
A17: yy in dom tyn and
A18: z = tyn . yy by FUNCT_1:def 5;
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:9;
then A19: DigA ty,yy is Element of k -SD by RADIX_1:19;
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:9;
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 H₃( Nat) -> Element of K455() = 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 = H₃(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 set ; :: 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 set such that
A26: zz in dom tzn and
A27: z = tzn . zz by FUNCT_1:def 5;
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:9;
then A28: DigA tz,zz is Element of k -SD by RADIX_1:19;
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:9;
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 H₄( Nat) -> Element of K455() = 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 = H₄(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 set ; :: 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 set such that
A35: ww in dom twn and
A36: w = twn . ww by FUNCT_1:def 5;
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:9;
then A37: DigA tw,ww is Element of k -SD by RADIX_1:19;
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:9;
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 13;
twn is Element of n -tuples_on (k -SD ) by A32, FINSEQ_2:110;
then reconsider twn = twn as Tuple of n,k -SD by A32, FINSEQ_2:151;
tzn is Element of n -tuples_on (k -SD ) by A23, FINSEQ_2:110;
then reconsider tzn = tzn as Tuple of n,k -SD by A23, FINSEQ_2:151;
tyn is Element of n -tuples_on (k -SD ) by A14, FINSEQ_2:110;
then reconsider tyn = tyn as Tuple of n,k -SD by A14, FINSEQ_2:151;
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:5;
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:110;
then reconsider txn = txn as Tuple of n,k -SD by A5, FINSEQ_2:151;
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:3;
then A46: i <= n + 1 by NAT_1:12;
1 <= i by A45, FINSEQ_1:3;
then A47: i in Seg (n + 1) by A46, FINSEQ_1:3;
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: S₁[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:3;
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:234
.= (SD_Add_Data ((DigA tx,1) + (DigA ty,1)),k) + (SD_Add_Carry ((DigA tx,0 ) + (DigA ty,0 ))) by XREAL_1:234
.= (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:234
.= (SD_Add_Data ((DigA tz,1) + (DigA tw,1)),k) + (SD_Add_Carry ((DigA tz,0 ) + (DigA tw,0 ))) by XREAL_1:234
.= (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
S₁[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