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