let I be set ; :: thesis: for A being ManySortedSet of I st union A is finite-yielding holds
( A is finite-yielding & ( for M being ManySortedSet of I st M in A holds
M is finite-yielding ) )
let A be ManySortedSet of I; :: thesis: ( union A is finite-yielding implies ( A is finite-yielding & ( for M being ManySortedSet of I st M in A holds
M is finite-yielding ) ) )
assume A1: union A is finite-yielding ; :: thesis: ( A is finite-yielding & ( for M being ManySortedSet of I st M in A holds
M is finite-yielding ) )
thus A is finite-yielding :: thesis: for M being ManySortedSet of I st M in A holds
M is finite-yielding

proof

let i be object ; :: according to FINSET_1:def 5 :: thesis: ( not i in I or A . i is finite )
assume A2: i in I ; :: thesis: A . i is finite
(union A) . i is finite by A1;
then union (A . i) is finite by A2, MBOOLEAN:def 2;
hence A . i is finite by FINSET_1:7; :: thesis: verum

end;

let M be ManySortedSet of I; :: thesis: ( M in A implies M is finite-yielding )
assume A3: M in A ; :: thesis: M is finite-yielding
let i be object ; :: according to FINSET_1:def 5 :: thesis: ( not i in I or M . i is finite )
assume A4: i in I ; :: thesis: M . i is finite
(union A) . i is finite by A1;
then A5: union (A . i) is finite by A4, MBOOLEAN:def 2;
M . i in A . i by A3, A4;
hence M . i is finite by A5, FINSET_1:7; :: thesis: verum