let SF be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for x, y, z being Element of SF st x * y = x * z & x <> 0. SF holds
y = z
let x, y, z be Element of SF; :: thesis: ( x * y = x * z & x <> 0. SF implies y = z )
assume that
A1: x * y = x * z and
A2: x <> 0. SF ; :: thesis: y = z
consider u being Element of SF such that
A3: x * u = 1_ SF by A2, Th6;
A4: u * x = 1_ SF by A3, Th7;
then y = (u * x) * y
.= u * (x * z) by A1, GROUP_1:def 3
.= (1_ SF) * z by A4, GROUP_1:def 3
.= z ;
hence y = z ; :: thesis: verum