let x, y be Element of REAL ; :: thesis: [*x,y*] = x + (y * <i>)
A1: Im (x + (y * <i>)) = (Im x) + (Im (y * <i>)) by Lm18
.= 0 + (Im (y * <i>))
.= y by Lm20 ;
Re (x + (y * <i>)) = (Re x) + (Re (y * <i>)) by Lm18
.= (Re x) + 0 by Lm19
.= x by Def1 ;
hence [*x,y*] = x + (y * <i>) by A1, Lm3; :: thesis: verum