let x, a, y, b, z be Element of COMPLEX ; :: thesis: x .|. ((a * y) + (b * z)) = ((a *') * (x .|. y)) + ((b *') * (x .|. z))
thus x .|. ((a * y) + (b * z)) = (x .|. (a * y)) + (x .|. (b * z)) by Th49
.= ((a *') * (x .|. y)) + (x .|. (b * z)) by Th51
.= ((a *') * (x .|. y)) + ((b *') * (x .|. z)) by Th51 ; :: thesis: verum