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 Th45
.= ((x .|. x) - (x .|. y)) - ((y .|. x) - (y .|. y)) by Th45
.= (((x .|. x) - (x .|. y)) - (y .|. x)) + (y .|. y) ;
hence (x - y) .|. (x - y) = (((x .|. x) - (x .|. y)) - (y .|. x)) + (y .|. y) ; :: thesis: verum