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

(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