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