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 & ( 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 Def26;
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 ) ) by Def24; :: 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 :: 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 ) )

proof

let a, x, y be Element of L; :: thesis: ( a <> 0. L & a * x = a * y implies x = y )
assume A3: a <> 0. L ; :: thesis: ( not a * x = a * y or x = y )
L is almost_left_cancelable by A2;
then a is left_mult-cancelable by A3, ALGSTR_0:def 36;
hence ( not a * x = a * y or x = y ) by ALGSTR_0:def 20; :: thesis: verum

end;

thus for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y :: 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 ) )

proof

let a, x, y be Element of L; :: thesis: ( a <> 0. L & x * a = y * a implies x = y )
assume A4: a <> 0. L ; :: thesis: ( not x * a = y * a or x = y )
L is almost_right_cancelable by A2;
then a is right_mult-cancelable by A4, ALGSTR_0:def 37;
hence ( not x * a = y * a or x = y ) by ALGSTR_0:def 21; :: thesis: verum

end;

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, Def26; :: thesis: verum

end;

assume A5: ( ( 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 ) ) ; :: thesis: L is multLoop_0-like
A6: L is almost_left_cancelable

proof

let x be Element of L; :: according to ALGSTR_0:def 36 :: thesis: ( x = 0. L or x is left_mult-cancelable )
assume A7: 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 A5, A7; :: thesis: verum

end;

L is almost_right_cancelable

proof

let x be Element of L; :: according to ALGSTR_0:def 37 :: 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;

then ( L is almost_invertible & L is almost_cancelable & ( 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 A5, A6, Def24;
hence L is multLoop_0-like by Def26; :: thesis: verum