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 S is finite & card (Union 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 S is finite & card (Union 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 S is finite & card (Union S) = Sum L )
hence ( Union S is finite & card (Union S) = Sum L ) by A1, Lm2; :: thesis: verum