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

proof

let X' be set ; :: thesis: ( X' in A . i implies X' is finite )
assume A5: X' in A . i ; :: thesis: X' is finite
consider M being ManySortedSet of I such that
A6: M in A by PBOOLE:146;
A7: dom (i .--> X') = {i} by FUNCOP_1:19;
dom (M +* (i .--> X')) = I by A3, PZFMISC1:1;
then reconsider K = M +* (i .--> X') as ManySortedSet of I by PBOOLE:def 3;
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 A5, 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 A6, A9, PBOOLE:def 4; :: thesis: verum

end;

end;

end;

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

end;

then K is locally-finite by A2;
hence X' is finite by A3, A8, PRE_CIRC:def 3; :: thesis: verum

end;

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