let th be Real; :: thesis: ( cos . th = Sum (th P_cos) & sin . th = Sum (th P_sin) )
reconsider th = th as Real ;
( sin . th = Im (Sum ((th * <i>) ExpSeq)) & cos . th = Re (Sum ((th * <i>) ExpSeq)) ) by Def16, Def18;
hence ( cos . th = Sum (th P_cos) & sin . th = Sum (th P_sin) ) by Th35; :: thesis: verum