let S be Function; :: thesis: for L being FinSequence of NAT st S is disjoint_valued & dom S = dom L & ( for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) ) holds
( union (rng S) is finite & card (union (rng S)) = Sum L )
let L be FinSequence of NAT ; :: thesis: ( S is disjoint_valued & dom S = dom L & ( for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) ) implies ( union (rng S) is finite & card (union (rng S)) = Sum L ) )
A1: len L is Element of NAT ;
assume ( S is disjoint_valued & dom S = dom L & ( for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) ) ) ; :: thesis: ( union (rng S) is finite & card (union (rng S)) = Sum L )
hence ( union (rng S) is finite & card (union (rng S)) = Sum L ) by A1, Th17; :: thesis: verum