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

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