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