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 AS: ( 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
P1: S is disjoint_valued by AS, LmDefREQ43;
P2: for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) by AS, LmDefREQ42;
Union S = X by LmDefREQ44, AS;
hence card X = Sum L by AS, P1, P2, DIST_1:18; :: thesis: verum