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