let I be set ; :: thesis: for A being non-empty finite-yielding ManySortedSet of I 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 non-empty finite-yielding ManySortedSet of I; :: 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 object ; :: according to PBOOLE:def 1 :: 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 2;
then A . i in rng A by FUNCT_1:3;
then A3: A . i is finite by FINSET_1:def 2;
A4: for X9, Y9 being set st X9 in A . i & Y9 in A . i & not X9 c= Y9 holds
Y9 c= X9

proof

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

proof

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

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

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

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

end;

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

then not j in dom (i .--> Y9) by TARSKI:def 1;
then K2 . j = M . j by FUNCT_4:11;
hence K2 . j in A . j by A7, A13; :: thesis: verum

end;

end;

end;

dom (i .--> X9) = {i} ;
then A15: K1 . i = (i .--> X9) . i by A9, FUNCT_4:13
.= X9 by FUNCOP_1:72 ;
K1 in A

proof

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

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

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

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

end;

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

then not j in dom (i .--> X9) by TARSKI:def 1;
then K1 . j = M . j by FUNCT_4:11;
hence K1 . j in A . j by A7, A16; :: thesis: verum

end;

end;

end;

then ( K1 c= K2 or K2 c= K1 ) by A1, A12;
hence Y9 c= X9 by A2, A8, A15, A11; :: thesis: verum

end;

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