let L be non empty multLoopStr_0 ; :: thesis: ( L is multLoop_0-like iff ( ( for a, b being Element of L st a <> 0. L holds

ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds

ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds

x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds

x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) ) )

A3: ( ( for a, b being Element of L st a <> 0. L holds

ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds

ex x being Element of L st x * a = b ) ) and

A4: for a, x, y being Element of L st a <> 0. L & a * x = a * y holds

x = y and

A5: for a, x, y being Element of L st a <> 0. L & x * a = y * a holds

x = y and

A6: ( ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) ) ; :: thesis: L is multLoop_0-like

A7: L is almost_right_cancelable

hence L is multLoop_0-like by A6; :: thesis: verum

ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds

ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds

x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds

x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) ) )

hereby :: thesis: ( ( for a, b being Element of L st a <> 0. L holds

ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds

ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds

x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds

x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) implies L is multLoop_0-like )

assume that ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds

ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds

x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds

x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) implies L is multLoop_0-like )

assume A1:
L is multLoop_0-like
; :: thesis: ( ( for a, b being Element of L st a <> 0. L holds

ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds

ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds

x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds

x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) )

then A2: ( L is almost_invertible & L is almost_cancelable ) ;

hence ( ( for a, b being Element of L st a <> 0. L holds

ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds

ex x being Element of L st x * a = b ) ) ; :: thesis: ( ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds

x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds

x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) )

thus for a, x, y being Element of L st a <> 0. L & a * x = a * y holds

x = y by A2, ALGSTR_0:def 20, ALGSTR_0:def 36; :: thesis: ( ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds

x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) )

thus for a, x, y being Element of L st a <> 0. L & x * a = y * a holds

x = y by A2, ALGSTR_0:def 21, ALGSTR_0:def 37; :: thesis: ( ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) )

thus ( ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) ) by A1; :: thesis: verum

end;ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds

ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds

x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds

x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) )

then A2: ( L is almost_invertible & L is almost_cancelable ) ;

hence ( ( for a, b being Element of L st a <> 0. L holds

ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds

ex x being Element of L st x * a = b ) ) ; :: thesis: ( ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds

x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds

x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) )

thus for a, x, y being Element of L st a <> 0. L & a * x = a * y holds

x = y by A2, ALGSTR_0:def 20, ALGSTR_0:def 36; :: thesis: ( ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds

x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) )

thus for a, x, y being Element of L st a <> 0. L & x * a = y * a holds

x = y by A2, ALGSTR_0:def 21, ALGSTR_0:def 37; :: thesis: ( ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) )

thus ( ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) ) by A1; :: thesis: verum

A3: ( ( for a, b being Element of L st a <> 0. L holds

ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds

ex x being Element of L st x * a = b ) ) and

A4: for a, x, y being Element of L st a <> 0. L & a * x = a * y holds

x = y and

A5: for a, x, y being Element of L st a <> 0. L & x * a = y * a holds

x = y and

A6: ( ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) ) ; :: thesis: L is multLoop_0-like

A7: L is almost_right_cancelable

proof

L is almost_left_cancelable
let x be Element of L; :: according to ALGSTR_0:def 36 :: thesis: ( x = 0. L or x is right_mult-cancelable )

assume A8: x <> 0. L ; :: thesis: x is right_mult-cancelable

let y, z be Element of L; :: according to ALGSTR_0:def 21 :: thesis: ( not y * x = z * x or y = z )

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

hence y = z by A5, A8; :: thesis: verum

end;assume A8: x <> 0. L ; :: thesis: x is right_mult-cancelable

let y, z be Element of L; :: according to ALGSTR_0:def 21 :: thesis: ( not y * x = z * x or y = z )

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

hence y = z by A5, A8; :: thesis: verum

proof

then
( L is almost_invertible & L is almost_cancelable )
by A3, A7;
let x be Element of L; :: according to ALGSTR_0:def 35 :: thesis: ( x = 0. L or x is left_mult-cancelable )

assume A9: x <> 0. L ; :: thesis: x is left_mult-cancelable

let y, z be Element of L; :: according to ALGSTR_0:def 20 :: thesis: ( not x * y = x * z or y = z )

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

hence y = z by A4, A9; :: thesis: verum

end;assume A9: x <> 0. L ; :: thesis: x is left_mult-cancelable

let y, z be Element of L; :: according to ALGSTR_0:def 20 :: thesis: ( not x * y = x * z or y = z )

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

hence y = z by A4, A9; :: thesis: verum

hence L is multLoop_0-like by A6; :: thesis: verum