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