reconsider t = sqrt a as Element of NAT by ORDINAL1:def 12;
reconsider q = sqrt b as Element of NAT by ORDINAL1:def 12;
A1: ( t ^2 = a & q ^2 = b ) by SQUARE_1:def 2;
(t ^2) gcd (q ^2) = (t gcd q) ^2 by NEWTON02:7;
hence a gcd b is square by A1; :: thesis: verum