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