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