let L be non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr ; :: thesis: for z, z1 being Element of L st z <> 0. L holds
z1 = (z1 * z) / z
let z, z1 be Element of L; :: thesis: ( z <> 0. L implies z1 = (z1 * z) / z )
assume A1: z <> 0. L ; :: thesis: z1 = (z1 * z) / z
thus (z1 * z) / z = z1 * (z * (z ")) by GROUP_1:def 3
.= z1 * (1. L) by A1, VECTSP_1:def 10
.= z1 ; :: thesis: verum