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 Th36
.= ((a *') * (x .|. y)) + (x .|. (b * z)) by Th38
.= ((a *') * (x .|. y)) + ((b *') * (x .|. z)) by Th38 ; :: thesis: verum