set M = Trivial-multLoopStr ;
thus Trivial-multLoopStr is left_mult-cancelable :: according to ALGSTR_0:def 25 :: thesis: Trivial-multLoopStr is right_mult-cancelable
proof
let x, y, z be Element of Trivial-multLoopStr; :: according to ALGSTR_0:def 20,ALGSTR_0:def 23 :: 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, y, z be Element of Trivial-multLoopStr; :: according to ALGSTR_0:def 21,ALGSTR_0:def 24 :: 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