let F, G be Cardinal-Function; :: thesis: ( dom F = dom G & ( for x being set st x in dom F holds
F . x c= G . x ) implies Sum F c= Sum G )
assume A1: ( dom F = dom G & ( for x being set st x in dom F holds
F . x c= G . x ) ) ; :: thesis: Sum F c= Sum G
Union (disjoin F) c= Union (disjoin G)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Union (disjoin F) or x in Union (disjoin G) )
assume x in Union (disjoin F) ; :: thesis: x in Union (disjoin G)
then consider X being set such that
A2: ( x in X & X in rng (disjoin F) ) by TARSKI:def 4;
consider y being set such that
A3: ( y in dom (disjoin F) & X = (disjoin F) . y ) by A2, FUNCT_1:def 5;
y in dom F by A3, Def3;
then ( F . y c= G . y & X = [:(F . y),{y}:] & (disjoin G) . y = [:(G . y),{y}:] & F . y = F . y & G . y = G . y & y in dom (disjoin G) ) by A1, A3, Def3;
then ( X c= [:(G . y),{y}:] & [:(G . y),{y}:] in rng (disjoin G) ) by FUNCT_1:def 5, ZFMISC_1:118;
hence x in Union (disjoin G) by A2, TARSKI:def 4; :: thesis: verum

end;

hence Sum F c= Sum G by CARD_1:27; :: thesis: verum