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:25; :: thesis: verum