let I be set ; :: thesis: for A, B being ManySortedSet of I st A c= B & B is V36() holds
A is V36()
let A, B be ManySortedSet of I; :: thesis: ( A c= B & B is V36() implies A is V36() )
assume A1: ( A c= B & B is V36() ) ; :: thesis: A is V36()
let i be set ; :: according to FINSET_1:def 5 :: thesis: ( not i in I or A . i is finite )
assume i in I ; :: thesis: A . i is finite
then ( A . i c= B . i & B . i is finite ) by A1, PBOOLE:def 2;
hence A . i is finite ; :: thesis: verum