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 ) ) )

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 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;

assume that
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

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;

L is almost_left_cancelable

proof

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;

then ( L is almost_invertible & L is almost_cancelable ) by A3, A7;
hence L is multLoop_0-like by A6; :: thesis: verum