let R be commutative Ring; :: thesis: for a, b being Element of R st a is square & b is square holds
a * b is square
let a, b be Element of R; :: thesis: ( a is square & b is square implies a * b is square )
assume AS: ( a is square & b is square ) ; :: thesis: a * b is square
then consider x being Element of R such that
A: a = x ^2 ;
consider y being Element of R such that
B: b = y ^2 by AS;
a * b = x * (x * (y * y)) by GROUP_1:def 3, A, B
.= x * (y * (x * y)) by GROUP_1:def 3
.= (x * y) ^2 by GROUP_1:def 3 ;
hence a * b is square ; :: thesis: verum