let x, y be Element of COMPLEX ; :: thesis: Im (x .|. y) = (- ((Re x) * (Im y))) + ((Im x) * (Re y))
x .|. y = (((Re x) * (Re y)) + ((Im x) * (Im y))) + (((- ((Re x) * (Im y))) + ((Im x) * (Re y))) * <i>) by COMPLEX2:29;
hence Im (x .|. y) = (- ((Re x) * (Im y))) + ((Im x) * (Re y)) by COMPLEX1:12; :: thesis: verum