let F be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; :: thesis: for x, y, z being Element of F st x <> 0. F & x * y = x * z holds
y = z
let x, y, z be Element of F; :: thesis: ( x <> 0. F & x * y = x * z implies y = z )
assume x <> 0. F ; :: thesis: ( not x * y = x * z or y = z )
then consider x1 being Element of F such that
A1: x1 * x = 1. F by Def9;
A2: ( (x1 * x) * y = x1 * (x * y) & x1 * (x * z) = (x1 * x) * z ) by GROUP_1:def 3;
assume x * y = x * z ; :: thesis: y = z
then (x * x1) * y = z by A1, A2, Def8;
hence y = z by A1; :: thesis: verum