let a, x, y be Element of COMPLEX ; :: thesis: (a * x) .|. y = x .|. ((a *' ) * y)
thus (a * x) .|. y = x * (((a *' ) *' ) * (y *' ))
.= x .|. ((a *' ) * y) by COMPLEX1:121 ; :: thesis: verum