let x, y be Complex; :: thesis: x .|. y = (((Re x) * (Re y)) + ((Im x) * (Im y))) + (((- ((Re x) * (Im y))) + ((Im x) * (Re y))) * <i>)
( x = (Re x) + ((Im x) * <i>) & y *' = (Re y) - ((Im y) * <i>) ) by COMPLEX1:13, COMPLEX1:def 11;
hence x .|. y = (((Re x) * (Re y)) + ((Im x) * (Im y))) + (((- ((Re x) * (Im y))) + ((Im x) * (Re y))) * <i>) ; :: thesis: verum