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