set M = Trivial-multLoopStr_0 ;
thus Trivial-multLoopStr_0 is almost_left_cancelable by STRUCT_0:def 10; :: according to ALGSTR_0:def 37 :: thesis: Trivial-multLoopStr_0 is almost_right_cancelable
let x be Element of Trivial-multLoopStr_0; :: according to ALGSTR_0:def 36 :: 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