let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for x, v being Element of K st x <> 0. K holds
x * ((x ") * v) = v
let x, v be Element of K; :: thesis: ( x <> 0. K implies x * ((x ") * v) = v )
assume A1: x <> 0. K ; :: thesis: x * ((x ") * v) = v
thus x * ((x ") * v) = (x * (x ")) * v by GROUP_1:def 3
.= (1. K) * v by A1, VECTSP_2:def 2
.= v ; :: thesis: verum