let F, G be Cardinal-Function; :: thesis: ( F c= G implies Sum F c= Sum G )
assume F c= G ; :: thesis: Sum F c= Sum G
then disjoin F c= disjoin G by Th23;
hence Sum F c= Sum G by Th24, CARD_1:11; :: thesis: verum