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 FUNCT_4:def 8
.= h by A1 ; :: thesis: e * h = h
thus e * h = a * b by FUNCT_4:def 8
.= h by A1 ; :: thesis: verum