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