let x be non zero Element of N_Real; :: thesis: x is mult-cancelable
thus x is right_mult-cancelable by XCMPLX_1:5; :: according to ALGSTR_0:def 22 :: thesis: x is left_mult-cancelable
let y, z be Element of N_Real; :: according to ALGSTR_0:def 20 :: thesis: ( not x * y = x * z or y = z )
thus ( not x * y = x * z or y = z ) by XCMPLX_1:5; :: thesis: verum