let K be non empty well-unital doubleLoopStr ; :: thesis: for h, e being Element of (opp K) st e = 1. K holds
( h * e = h & e * h = h )
let h, e be Element of (opp K); :: thesis: ( e = 1. K implies ( h * e = h & e * h = h ) )
assume A1: e = 1. K ; :: thesis: ( h * e = h & e * h = h )
reconsider a = h, b = e as Element of K ;
thus h * e = b * a by Th1
.= h by A1, VECTSP_1:def 16 ; :: thesis: e * h = h
thus e * h = a * b by Th1
.= h by A1, VECTSP_1:def 16 ; :: thesis: verum