let I be set ; :: thesis: for A, B being ManySortedSet of I st A is non-empty & [|A,B|] is finite-yielding holds
B is finite-yielding
let A, B be ManySortedSet of I; :: thesis: ( A is non-empty & [|A,B|] is finite-yielding implies B is finite-yielding )
assume that
A1: A is non-empty and
A2: [|A,B|] is finite-yielding ; :: thesis: B is finite-yielding
let i be set ; :: according to FINSET_1:def 4 :: thesis: ( not i in I or B . i is finite )
assume A3: i in I ; :: thesis: B . i is finite
then [|A,B|] . i is finite by A2, Lm1;
then [:(A . i),(B . i):] is finite by A3, PBOOLE:def 16;
hence B . i is finite by A1, A3; :: thesis: verum