let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for a, b being Element of K st a <> 0. K holds

(a ") * (a * b) = b

let a, b be Element of K; :: thesis: ( a <> 0. K implies (a ") * (a * b) = b )

assume A1: a <> 0. K ; :: thesis: (a ") * (a * b) = b

thus (a ") * (a * b) = ((a ") * a) * b by GROUP_1:def 3

.= (1. K) * b by A1, VECTSP_2:def 2

.= b ; :: thesis: verum

(a ") * (a * b) = b

let a, b be Element of K; :: thesis: ( a <> 0. K implies (a ") * (a * b) = b )

assume A1: a <> 0. K ; :: thesis: (a ") * (a * b) = b

thus (a ") * (a * b) = ((a ") * a) * b by GROUP_1:def 3

.= (1. K) * b by A1, VECTSP_2:def 2

.= b ; :: thesis: verum