let L be non empty multLoopStr ; :: thesis: ( L is multGroup iff ( ( 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) ) ) )

thus ( L is multGroup implies ( ( 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) ) ) ) by Def6, GROUP_1:def 3; :: 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) ) implies L is multGroup )

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: L is multGroup

A4: for a, b being Element of L ex x being Element of L st x * a = b

thus ( L is multGroup implies ( ( 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) ) ) ) by Def6, GROUP_1:def 3; :: 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) ) implies L is multGroup )

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: L is multGroup

A4: for a, b being Element of L ex x being Element of L st x * a = b

proof

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

consider y being Element of L such that

A5: y * a = 1. L by A1, A2, A3, Lm13;

take x = b * y; :: thesis: x * a = b

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

.= b by A1 ; :: thesis: verum

end;consider y being Element of L such that

A5: y * a = 1. L by A1, A2, A3, Lm13;

take x = b * y; :: thesis: x * a = b

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

.= b by A1 ; :: thesis: verum

proof

A7:
L is left_mult-cancelable
let a be Element of L; :: thesis: (1. L) * a = a

thus (1. L) * a = a * (1. L) by A1, A2, A3, Lm12

.= a by A1 ; :: thesis: verum

end;thus (1. L) * a = a * (1. L) by A1, A2, A3, Lm12

.= a by A1 ; :: thesis: verum

proof

A9:
L is right_mult-cancelable
let a be Element of L; :: according to ALGSTR_0:def 23 :: thesis: a is left_mult-cancelable

let x be Element of L; :: according to ALGSTR_0:def 20 :: thesis: for b_{1} being Element of the carrier of L holds

( not a * x = a * b_{1} or x = b_{1} )

let y be Element of L; :: thesis: ( not a * x = a * y or x = y )

consider z being Element of L such that

A8: z * a = 1. L by A1, A2, A3, Lm13;

assume a * x = a * y ; :: thesis: x = y

then (z * a) * x = z * (a * y) by A3

.= (z * a) * y by A3 ;

hence x = (1. L) * y by A6, A8

.= y by A6 ;

:: thesis: verum

end;let x be Element of L; :: according to ALGSTR_0:def 20 :: thesis: for b

( not a * x = a * b

let y be Element of L; :: thesis: ( not a * x = a * y or x = y )

consider z being Element of L such that

A8: z * a = 1. L by A1, A2, A3, Lm13;

assume a * x = a * y ; :: thesis: x = y

then (z * a) * x = z * (a * y) by A3

.= (z * a) * y by A3 ;

hence x = (1. L) * y by A6, A8

.= y by A6 ;

:: thesis: verum

proof

for a, b being Element of L ex x being Element of L st a * x = b
let a be Element of L; :: according to ALGSTR_0:def 24 :: thesis: a is right_mult-cancelable

let x be Element of L; :: according to ALGSTR_0:def 21 :: thesis: for b_{1} being Element of the carrier of L holds

( not x * a = b_{1} * a or x = b_{1} )

let y be Element of L; :: thesis: ( not x * a = y * a or x = y )

consider z being Element of L such that

A10: a * z = 1. L by A2;

assume x * a = y * a ; :: thesis: x = y

then x * (a * z) = (y * a) * z by A3

.= y * (a * z) by A3 ;

hence x = y * (1. L) by A1, A10

.= y by A1 ;

:: thesis: verum

end;let x be Element of L; :: according to ALGSTR_0:def 21 :: thesis: for b

( not x * a = b

let y be Element of L; :: thesis: ( not x * a = y * a or x = y )

consider z being Element of L such that

A10: a * z = 1. L by A2;

assume x * a = y * a ; :: thesis: x = y

then x * (a * z) = (y * a) * z by A3

.= y * (a * z) by A3 ;

hence x = y * (1. L) by A1, A10

.= y by A1 ;

:: thesis: verum

proof

hence
L is multGroup
by A1, A3, A6, A4, A7, A9, Def6, GROUP_1:def 3, VECTSP_1:def 6; :: thesis: verum
let a, b be Element of L; :: thesis: ex x being Element of L st a * x = b

consider y being Element of L such that

A11: a * y = 1. L by A2;

take x = y * b; :: thesis: a * x = b

thus a * x = (1. L) * b by A3, A11

.= b by A6 ; :: thesis: verum

end;consider y being Element of L such that

A11: a * y = 1. L by A2;

take x = y * b; :: thesis: a * x = b

thus a * x = (1. L) * b by A3, A11

.= b by A6 ; :: thesis: verum