let F, G be Cardinal-Function; :: thesis: ( dom F = dom G & ( for x being object st x in dom F holds
F . x c= G . x ) implies Sum F c= Sum G )
assume that
A1: dom F = dom G and
A2: for x being object 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 object ; :: 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
A3: x in X and
A4: X in rng (disjoin F) by TARSKI:def 4;
consider y being object such that
A5: y in dom (disjoin F) and
A6: X = (disjoin F) . y by A4, FUNCT_1:def 3;
A7: y in dom F by A5, Def3;
then A8: F . y c= G . y by A2;
A9: X = [:(F . y),{y}:] by A6, A7, Def3;
A10: (disjoin G) . y = [:(G . y),{y}:] by A1, A7, Def3;
A11: y in dom (disjoin G) by A1, A7, Def3;
A12: X c= [:(G . y),{y}:] by A8, A9, ZFMISC_1:95;
[:(G . y),{y}:] in rng (disjoin G) by A10, A11, FUNCT_1:def 3;
hence x in Union (disjoin G) by A3, A12, TARSKI:def 4; :: thesis: verum

end;

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