consider n' being Nat such that
A1: n = n' ^2 by Def3;
consider m' being Nat such that
A2: m = m' ^2 by Def3;
m * n = (m' * n') ^2 by A2, A1;
hence m * n is square ; :: thesis: verum