let G be Group; :: thesis: for h being Element of G holds h |^ 2 = h * h
let h be Element of G; :: thesis: h |^ 2 = h * h
thus h |^ 2 = h |^ (1 + 1)
.= (h |^ 1) * h by Def7
.= h * h by Th25 ; :: thesis: verum