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