let n be Nat; :: thesis: ( n >= 1 implies for m, k being Nat st m is_represented_by n,k holds

m = SDDec2 ((DecSD2 (m,n,k)),k) )

assume A1: n >= 1 ; :: thesis: for m, k being Nat st m is_represented_by n,k holds

m = SDDec2 ((DecSD2 (m,n,k)),k)

let m, k be Nat; :: thesis: ( m is_represented_by n,k implies m = SDDec2 ((DecSD2 (m,n,k)),k) )

assume A2: m is_represented_by n,k ; :: thesis: m = SDDec2 ((DecSD2 (m,n,k)),k)

SDDec2 ((DecSD2 (m,n,k)),k) = SDDec (DecSD (m,n,k)) by Th13, Th14;

hence m = SDDec2 ((DecSD2 (m,n,k)),k) by A1, A2, RADIX_1:22; :: thesis: verum

m = SDDec2 ((DecSD2 (m,n,k)),k) )

assume A1: n >= 1 ; :: thesis: for m, k being Nat st m is_represented_by n,k holds

m = SDDec2 ((DecSD2 (m,n,k)),k)

let m, k be Nat; :: thesis: ( m is_represented_by n,k implies m = SDDec2 ((DecSD2 (m,n,k)),k) )

assume A2: m is_represented_by n,k ; :: thesis: m = SDDec2 ((DecSD2 (m,n,k)),k)

SDDec2 ((DecSD2 (m,n,k)),k) = SDDec (DecSD (m,n,k)) by Th13, Th14;

hence m = SDDec2 ((DecSD2 (m,n,k)),k) by A1, A2, RADIX_1:22; :: thesis: verum