let X be non empty finite set ; :: thesis: for R being Equivalence_Relation of X
for S being Class b₁ -valued Function
for L being FinSequence of NAT st S is one-to-one & S is onto & dom S = dom L & ( for i being Nat st i in dom S holds
L . i = card (S . i) ) holds
card X = Sum L
let R be Equivalence_Relation of X; :: thesis: for S being Class R -valued Function
for L being FinSequence of NAT st S is one-to-one & S is onto & dom S = dom L & ( for i being Nat st i in dom S holds
L . i = card (S . i) ) holds
card X = Sum L
let S be Class R -valued Function; :: thesis: for L being FinSequence of NAT st S is one-to-one & S is onto & dom S = dom L & ( for i being Nat st i in dom S holds
L . i = card (S . i) ) holds
card X = Sum L
let L be FinSequence of NAT ; :: thesis: ( S is one-to-one & S is onto & dom S = dom L & ( for i being Nat st i in dom S holds
L . i = card (S . i) ) implies card X = Sum L )
assume A1: ( S is one-to-one & S is onto & dom S = dom L & ( for i being Nat st i in dom S holds
L . i = card (S . i) ) ) ; :: thesis: card X = Sum L
A2: S is disjoint_valued by A1, Th55;
A3: for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) by A1, Th54;
Union S = X by Th56, A1;
hence card X = Sum L by A1, A2, A3, DIST_1:17; :: thesis: verum