let L be non empty right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for x, y being Element of L st x <> 0. L & y <> 0. L holds
(x * y) " = (x ") * (y ")
let x, y be Element of L; :: thesis: ( x <> 0. L & y <> 0. L implies (x * y) " = (x ") * (y ") )
assume that
A1: x <> 0. L and
A2: y <> 0. L ; :: thesis: (x * y) " = (x ") * (y ")
A3: ((x ") * (y ")) * (x * y) = (((x ") * (y ")) * y) * x by GROUP_1:def 4
.= ((x ") * ((y ") * y)) * x by GROUP_1:def 4
.= ((x ") * (1. L)) * x by A2, VECTSP_1:def 22
.= (x ") * x by VECTSP_1:def 13
.= 1. L by A1, VECTSP_1:def 22 ;
x * y <> 0. L by A1, A2, VECTSP_1:44;
hence (x * y) " = (x ") * (y ") by A3, VECTSP_1:def 22; :: thesis: verum