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 Def14, GROUP_1:def 4, VECTSP_1:def 16; :: 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 A1: ( ( 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) ) ) ; :: thesis: L is multGroup

now

thus A2: for a being Element of L holds (1. L) * a = a :: thesis: ( ( for a, b being Element of L ex x being Element of L st a * x = b ) & ( for a, b being Element of L ex x being Element of L st x * a = b ) & L is left_mult-cancelable & L is right_mult-cancelable )

proof

let a be Element of L; :: thesis: (1. L) * a = a
thus (1. L) * a = a * (1. L) by A1, Lm17
.= a by A1 ; :: thesis: verum

end;

thus for a, b being Element of L ex x being Element of L st a * x = b :: thesis: ( ( for a, b being Element of L ex x being Element of L st x * a = b ) & L is left_mult-cancelable & L is right_mult-cancelable )

proof

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
A3: a * y = 1. L by A1;
take x = y * b; :: thesis: a * x = b
thus a * x = (1. L) * b by A1, A3
.= b by A2 ; :: thesis: verum

end;

thus for a, b being Element of L ex x being Element of L st x * a = b :: thesis: ( L is left_mult-cancelable & L is right_mult-cancelable )

proof

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
A4: y * a = 1. L by A1, Lm18;
take x = b * y; :: thesis: x * a = b
thus x * a = b * (1. L) by A1, A4
.= b by A1 ; :: thesis: verum

end;

thus L is left_mult-cancelable :: thesis: L is right_mult-cancelable

proof

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₁ being Element of the carrier of L holds
( not a * x = a * b₁ or x = b₁ )
let y be Element of L; :: thesis: ( not a * x = a * y or x = y )
consider z being Element of L such that
A5: z * a = 1. L by A1, Lm18;
assume a * x = a * y ; :: thesis: x = y
then (z * a) * x = z * (a * y) by A1
.= (z * a) * y by A1 ;
hence x = (1. L) * y by A2, A5
.= y by A2 ;
:: thesis: verum

end;

thus L is right_mult-cancelable :: thesis: verum

proof

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₁ being Element of the carrier of L holds
( not x * a = b₁ * a or x = b₁ )
let y be Element of L; :: thesis: ( not x * a = y * a or x = y )
consider z being Element of L such that
A6: a * z = 1. L by A1;
assume x * a = y * a ; :: thesis: x = y
then x * (a * z) = (y * a) * z by A1
.= y * (a * z) by A1 ;
hence x = y * (1. L) by A1, A6
.= y by A1 ;
:: thesis: verum

end;

end;

hence L is multGroup by A1, Def14, GROUP_1:def 4, VECTSP_1:def 16; :: thesis: verum