let F, G be Cardinal-Function; ( 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
; Sum F c= Sum G
Union (disjoin F) c= Union (disjoin G)
proof
let x be
object ;
TARSKI:def 3 ( not x in Union (disjoin F) or x in Union (disjoin G) )
assume
x in Union (disjoin F)
;
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;
verum
end;
hence
Sum F c= Sum G
by CARD_1:11; verum