let I be set ; :: thesis: for A being V2() V27() ManySortedSet of st ( for X, Y being ManySortedSet of I st X in A & Y in A & not X c= Y holds
Y c= X ) holds
union A in A
let A be V2() V27() ManySortedSet of ; :: thesis: ( ( for X, Y being ManySortedSet of I st X in A & Y in A & not X c= Y holds
Y c= X ) implies union A in A )
assume A1: for X, Y being ManySortedSet of I st X in A & Y in A & not X c= Y holds
Y c= X ; :: thesis: union A in A
let i be set ; :: according to PBOOLE:def 4 :: thesis: ( not i in I or (union A) . i in A . i )
assume A2: i in I ; :: thesis: (union A) . i in A . i
then i in dom A by PARTFUN1:def 4;
then A . i in rng A by FUNCT_1:12;
then A3: A . i is finite by FINSET_1:def 2;
A4: for X', Y' being set st X' in A . i & Y' in A . i & not X' c= Y' holds
Y' c= X'

proof

let X', Y' be set ; :: thesis: ( X' in A . i & Y' in A . i & not X' c= Y' implies Y' c= X' )
assume that
A5: X' in A . i and
A6: Y' in A . i ; :: thesis: ( X' c= Y' or Y' c= X' )
consider M being ManySortedSet of I such that
A7: M in A by PBOOLE:146;
( dom (M +* (i .--> Y')) = I & dom (M +* (i .--> X')) = I ) by A2, Lm1;
then reconsider K1 = M +* (i .--> X'), K2 = M +* (i .--> Y') as ManySortedSet of I by PARTFUN1:def 4, RELAT_1:def 18;
assume A8: not X' c= Y' ; :: thesis: Y' c= X'
A9: i in {i} by TARSKI:def 1;
A10: dom (i .--> Y') = {i} by FUNCOP_1:19;
then A11: K2 . i = (i .--> Y') . i by A9, FUNCT_4:14
.= Y' by FUNCOP_1:87 ;
A12: K2 in A

proof

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

now

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

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

hence K2 . j in A . j by A6, A11; :: thesis: verum

end;

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

then not j in dom (i .--> Y') by A10, TARSKI:def 1;
then K2 . j = M . j by FUNCT_4:12;
hence K2 . j in A . j by A7, A13, PBOOLE:def 4; :: thesis: verum

end;

end;

end;

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

end;

A14: dom (i .--> X') = {i} by FUNCOP_1:19;
then A15: K1 . i = (i .--> X') . i by A9, FUNCT_4:14
.= X' by FUNCOP_1:87 ;
K1 in A

proof

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

now

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

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

hence K1 . j in A . j by A5, A15; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

then ( K1 c= K2 or K2 c= K1 ) by A1, A12;
hence Y' c= X' by A2, A8, A15, A11, PBOOLE:def 5; :: thesis: verum

end;

A . i <> {} by A2, PBOOLE:def 16;
then union (A . i) in A . i by A3, A4, CARD_2:81;
hence (union A) . i in A . i by A2, Def2; :: thesis: verum