let I be set ; :: thesis: for Z being ManySortedSet of
for A being V2() ManySortedSet of st ( for X being ManySortedSet of st X in A holds
X c= Z ) holds
union A c= Z
let Z be ManySortedSet of ; :: thesis: for A being V2() ManySortedSet of st ( for X being ManySortedSet of st X in A holds
X c= Z ) holds
union A c= Z
let A be V2() ManySortedSet of ; :: thesis: ( ( for X being ManySortedSet of st X in A holds
X c= Z ) implies union A c= Z )
assume A1: for X being ManySortedSet of st X in A holds
X c= Z ; :: thesis: union A c= Z
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or (union A) . i c= Z . i )
assume A2: i in I ; :: thesis: (union A) . i c= Z . i
for X' being set st X' in A . i holds
X' c= Z . i

proof

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

end;

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

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

end;

end;

end;

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

end;

then K c= Z by A1;
hence X' c= Z . i by A2, A6, PBOOLE:def 5; :: thesis: verum

end;

then union (A . i) c= Z . i by ZFMISC_1:94;
hence (union A) . i c= Z . i by A2, Def2; :: thesis: verum