let x, y be Complex; :: thesis: (x + y) .|. (x + y) = (((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y)
(x + y) .|. (x + y) = (x .|. (x + y)) + (y .|. (x + y))
.= ((x .|. x) + (x .|. y)) + (y .|. (x + y)) by Th34
.= ((x .|. x) + (x .|. y)) + ((y .|. x) + (y .|. y)) by Th34
.= (((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y) ;
hence (x + y) .|. (x + y) = (((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y) ; :: thesis: verum