let th be real number ; :: thesis: ( cos . th = Sum (th P_cos ) & sin . th = Sum (th P_sin ) )
reconsider th = th as Real by XREAL_0:def 1;
A1: sin . th = Im (Sum ((th * <i> ) ExpSeq )) by Def20;
cos . th = Re (Sum ((th * <i> ) ExpSeq )) by Def22;
hence ( cos . th = Sum (th P_cos ) & sin . th = Sum (th P_sin ) ) by A1, Th39; :: thesis: verum