let th be Real; :: thesis: exp (th * <i> ) = (cos th) + ((sin th) * <i> )
A1: exp (th * <i> ) = Sum ((th * <i> ) ExpSeq ) by Def18
.= (cos th) + ((sin th) * <i> ) by Lm3 ;
thus exp (th * <i> ) = (cos th) + ((sin th) * <i> ) by A1; :: thesis: verum