let a, x, y be Complex; :: thesis: (a * x) .|. y = x .|. ((a *') * y)
thus (a * x) .|. y = x * (((a *') *') * (y *'))
.= x .|. ((a *') * y) by COMPLEX1:35 ; :: thesis: verum