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

( 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