let I be set ; :: thesis: for A being ManySortedSet of I st union A is V39() holds
( A is V39() & ( for M being ManySortedSet of I st M in A holds
M is V39() ) )
let A be ManySortedSet of I; :: thesis: ( union A is V39() implies ( A is V39() & ( for M being ManySortedSet of I st M in A holds
M is V39() ) ) )
assume A1: union A is V39() ; :: thesis: ( A is V39() & ( for M being ManySortedSet of I st M in A holds
M is V39() ) )
thus A is V39() :: thesis: for M being ManySortedSet of I st M in A holds
M is V39()
proof
let i be object ; :: according to FINSET_1:def 5 :: thesis: ( not i in I or A . i is finite )
assume A2: i in I ; :: thesis: A . i is finite
(union A) . i is finite by A1;
then union (A . i) is finite by A2, MBOOLEAN:def 2;
hence A . i is finite by FINSET_1:7; :: thesis: verum
end;
let M be ManySortedSet of I; :: thesis: ( M in A implies M is V39() )
assume A3: M in A ; :: thesis: M is V39()
let i be object ; :: according to FINSET_1:def 5 :: thesis: ( not i in I or M . i is finite )
assume A4: i in I ; :: thesis: M . i is finite
(union A) . i is finite by A1;
then A5: union (A . i) is finite by A4, MBOOLEAN:def 2;
M . i in A . i by A3, A4;
hence M . i is finite by A5, FINSET_1:7; :: thesis: verum