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