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

( 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