let L be non empty almost_left_invertible associative commutative well-unital distributive 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 4
.= z1 * (1. L) by A1, VECTSP_1:def 22
.= z1 by VECTSP_1:def 19 ; :: thesis: verum