let L be non empty multLoopStr ; :: thesis: for a, b being Element of L st ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & a * b = 1. L holds

b * a = 1. L

let a, b be Element of L; :: thesis: ( ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & a * b = 1. L implies b * a = 1. L )

assume that

A1: for a being Element of L holds a * (1. L) = a and

A2: for a being Element of L ex x being Element of L st a * x = 1. L and

A3: for a, b, c being Element of L holds (a * b) * c = a * (b * c) ; :: thesis: ( not a * b = 1. L or b * a = 1. L )

consider x being Element of L such that

A4: b * x = 1. L by A2;

assume A5: a * b = 1. L ; :: thesis: b * a = 1. L

thus b * a = (b * a) * (b * x) by A1, A4

.= ((b * a) * b) * x by A3

.= (b * (1. L)) * x by A3, A5

.= 1. L by A1, A4 ; :: thesis: verum

b * a = 1. L

let a, b be Element of L; :: thesis: ( ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & a * b = 1. L implies b * a = 1. L )

assume that

A1: for a being Element of L holds a * (1. L) = a and

A2: for a being Element of L ex x being Element of L st a * x = 1. L and

A3: for a, b, c being Element of L holds (a * b) * c = a * (b * c) ; :: thesis: ( not a * b = 1. L or b * a = 1. L )

consider x being Element of L such that

A4: b * x = 1. L by A2;

assume A5: a * b = 1. L ; :: thesis: b * a = 1. L

thus b * a = (b * a) * (b * x) by A1, A4

.= ((b * a) * b) * x by A3

.= (b * (1. L)) * x by A3, A5

.= 1. L by A1, A4 ; :: thesis: verum