let th be Real; :: thesis: Sum ((th * <i> ) ExpSeq ) = (cos . th) + ((sin . th) * <i> )
A1: ( Im (Sum ((th * <i> ) ExpSeq )) = sin . th & Re (Sum ((th * <i> ) ExpSeq )) = cos . th ) by Def20, Def22;
thus Sum ((th * <i> ) ExpSeq ) = (cos . th) + ((sin . th) * <i> ) by A1, COMPLEX1:29; :: thesis: verum