let I be set ; :: thesis: for A, B being ManySortedSet of st A c= B & B is finite-yielding holds
A is finite-yielding
let A, B be ManySortedSet of ; :: thesis: ( A c= B & B is finite-yielding implies A is finite-yielding )
assume that
A1: A c= B and
A2: B is finite-yielding ; :: thesis: A is finite-yielding
let i be set ; :: according to FINSET_1:def 4 :: thesis: ( not i in I or A . i is finite )
assume A3: i in I ; :: thesis: A . i is finite
then A4: A . i c= B . i by A1, PBOOLE:def 5;
B . i is finite by A2, A3, LL1;
hence A . i is finite by A4; :: thesis: verum