let x, y be Element of 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 Th60
.= ((x .|. x) - (x .|. y)) - ((y .|. x) - (y .|. y)) by Th60
.= (((x .|. x) - (x .|. y)) - (y .|. x)) + (y .|. y) ;
hence (x - y) .|. (x - y) = (((x .|. x) - (x .|. y)) - (y .|. x)) + (y .|. y) ; :: thesis: verum