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