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