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

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