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