let R be Ring; :: thesis: for a being Element of R holds a |^ 2 = a * a
let a be Element of R; :: thesis: a |^ 2 = a * a
a |^ (1 + 1) = (a |^ 1) * (a |^ 1) by BINOM:10
.= a * (a |^ 1) by BINOM:8
.= a * a by BINOM:8 ;
hence a |^ 2 = a * a ; :: thesis: verum