set M = Trivial-multLoopStr_0 ;
thus Trivial-multLoopStr_0 is almost_left_cancelable :: according to ALGSTR_0:def 38 :: thesis: Trivial-multLoopStr_0 is almost_right_cancelable

proof

let x be Element of Trivial-multLoopStr_0 ; :: according to ALGSTR_0:def 36 :: thesis: ( x <> 0. Trivial-multLoopStr_0 implies x is left_mult-cancelable )
assume x <> 0. Trivial-multLoopStr_0 ; :: thesis: x is left_mult-cancelable
let y, z be Element of Trivial-multLoopStr_0 ; :: according to ALGSTR_0:def 20 :: thesis: ( x * y = x * z implies y = z )
assume x * y = x * z ; :: thesis: y = z
thus y = z by STRUCT_0:def 10; :: thesis: verum

end;

let x be Element of Trivial-multLoopStr_0 ; :: according to ALGSTR_0:def 37 :: thesis: ( x <> 0. Trivial-multLoopStr_0 implies x is right_mult-cancelable )
assume x <> 0. Trivial-multLoopStr_0 ; :: thesis: x is right_mult-cancelable
let y, z be Element of Trivial-multLoopStr_0 ; :: according to ALGSTR_0:def 21 :: thesis: ( y * x = z * x implies y = z )
assume y * x = z * x ; :: thesis: y = z
thus y = z by STRUCT_0:def 10; :: thesis: verum