let I be set ; :: thesis: for A being V8() ManySortedSet of st A is finite-yielding & ( for M being ManySortedSet of I st M in A holds
M is finite-yielding ) holds
union A is finite-yielding
let A be V8() ManySortedSet of ; :: thesis: ( A is finite-yielding & ( for M being ManySortedSet of I st M in A holds
M is finite-yielding ) implies union A is finite-yielding )
assume that
A1: A is finite-yielding and
A2: for M being ManySortedSet of I st M in A holds
M is finite-yielding ; :: thesis: union A is finite-yielding
let i be set ; :: according to FINSET_1:def 4 :: thesis: ( not i in I or (union A) . i is finite )
assume A3: i in I ; :: thesis: (union A) . i is finite
A4: for X' being set st X' in A . i holds
X' is finite

proof

consider M being ManySortedSet of I such that
A5: M in A by PBOOLE:146;
let X' be set ; :: thesis: ( X' in A . i implies X' is finite )
assume A6: X' in A . i ; :: thesis: X' is finite
dom (M +* (i .--> X')) = I by A3, PZFMISC1:1;
then reconsider K = M +* (i .--> X') as ManySortedSet of I by PARTFUN1:def 4, RELAT_1:def 18;
A7: dom (i .--> X') = {i} by FUNCOP_1:19;
i in {i} by TARSKI:def 1;
then A8: K . i = (i .--> X') . i by A7, FUNCT_4:14
.= X' by FUNCOP_1:87 ;
K in A

proof

let j be set ; :: according to PBOOLE:def 4 :: thesis: ( not j in I or K . j in A . j )
assume A9: j in I ; :: thesis: K . j in A . j

now

per cases ( j = i or j <> i ) ;

case j = i ; :: thesis: K . j in A . j

hence K . j in A . j by A6, A8; :: thesis: verum

end;

case j <> i ; :: thesis: K . j in A . j

then not j in dom (i .--> X') by A7, TARSKI:def 1;
then K . j = M . j by FUNCT_4:12;
hence K . j in A . j by A5, A9, PBOOLE:def 4; :: thesis: verum

end;

end;

end;

hence K . j in A . j ; :: thesis: verum

end;

then K is finite-yielding by A2;
hence X' is finite by A3, A8, Lm1; :: thesis: verum

end;

A . i is finite by A1, A3, Lm1;
then union (A . i) is finite by A4, FINSET_1:25;
hence (union A) . i is finite by A3, MBOOLEAN:def 2; :: thesis: verum