let L be non empty right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative 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 3
.= ((x ") * ((y ") * y)) * x by GROUP_1:def 3
.= ((x ") * (1. L)) * x by A2, VECTSP_1:def 10
.= (x ") * x
.= 1. L by A1, VECTSP_1:def 10 ;
x * y <> 0. L by A1, A2, VECTSP_1:12;
hence (x * y) " = (x ") * (y ") by A3, VECTSP_1:def 10; :: thesis: verum