let I be set ; :: thesis: for A being ManySortedSet of I holds
( A is finite-yielding iff bool A is finite-yielding )
let A be ManySortedSet of I; :: thesis: ( A is finite-yielding iff bool A is finite-yielding )
thus ( A is finite-yielding implies bool A is finite-yielding ) :: thesis: ( bool A is finite-yielding implies A is finite-yielding )

proof

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

end;

assume A3: bool A is finite-yielding ; :: thesis: A is finite-yielding
let i be object ; :: according to FINSET_1:def 5 :: thesis: ( not i in I or A . i is finite )
assume A4: i in I ; :: thesis: A . i is finite
(bool A) . i is finite by A3;
then bool (A . i) is finite by A4, MBOOLEAN:def 1;
hence A . i is finite ; :: thesis: verum