let x, y be Element of 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:29, COMPLEX1:def 15;
hence x .|. y = (((Re x) * (Re y)) + ((Im x) * (Im y))) + (((- ((Re x) * (Im y))) + ((Im x) * (Re y))) * <i> ) ; :: thesis: verum