let I be non empty set ; :: thesis: for M being ManySortedSet of I
for x being Element of Bool M
for i being Element of I
for y being set st y in x . i holds
ex a being Element of Bool M st
( y in a . i & a is finite-yielding & support a is finite & a c= x )
let M be ManySortedSet of I; :: thesis: for x being Element of Bool M
for i being Element of I
for y being set st y in x . i holds
ex a being Element of Bool M st
( y in a . i & a is finite-yielding & support a is finite & a c= x )
let x be Element of Bool M; :: thesis: for i being Element of I
for y being set st y in x . i holds
ex a being Element of Bool M st
( y in a . i & a is finite-yielding & support a is finite & a c= x )
let i be Element of I; :: thesis: for y being set st y in x . i holds
ex a being Element of Bool M st
( y in a . i & a is finite-yielding & support a is finite & a c= x )
let y be set ; :: thesis: ( y in x . i implies ex a being Element of Bool M st
( y in a . i & a is finite-yielding & support a is finite & a c= x ) )
assume A1: y in x . i ; :: thesis: ex a being Element of Bool M st
( y in a . i & a is finite-yielding & support a is finite & a c= x )
set N = {i} --> {y};
set A = (EmptyMS I) +* ({i} --> {y});
A2: dom ({i} --> {y}) = {i} by FUNCOP_1:13;
then A3: i in dom ({i} --> {y}) by TARSKI:def 1;
then A4: ({i} --> {y}) . i = {y} by A2, FUNCOP_1:7;
then A5: ((EmptyMS I) +* ({i} --> {y})) . i = {y} by A3, FUNCT_4:13;
A6: dom ((EmptyMS I) +* ({i} --> {y})) = (dom (EmptyMS I)) \/ (dom ({i} --> {y})) by FUNCT_4:def 1
.= I \/ {i} by A2, PARTFUN1:def 2
.= I by ZFMISC_1:40 ;
then reconsider A = (EmptyMS I) +* ({i} --> {y}) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
for j being object st j in I holds
A . j c= M . j

proof

let j be object ; :: thesis: ( j in I implies A . j c= M . j )
assume A7: j in I ; :: thesis: A . j c= M . j

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

suppose A8: i = j ; :: thesis: A . j c= M . j

reconsider x = x as ManySortedSubset of M ;
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in A . j or v in M . j )
assume v in A . j ; :: thesis: v in M . j
then v in {y} by A3, A4, A8, FUNCT_4:13;
then A9: v in x . j by A1, A8, TARSKI:def 1;
x c= M by PBOOLE:def 18;
then x . j c= M . j by A7;
hence v in M . j by A9; :: thesis: verum

end;

suppose i <> j ; :: thesis: A . j c= M . j

then A10: not j in {i} by TARSKI:def 1;
j in (dom (EmptyMS I)) \/ (dom ({i} --> {y})) by A6, A7, FUNCT_4:def 1;
then A . j = (I --> {}) . j by A2, A10, FUNCT_4:def 1
.= {} by A7, FUNCOP_1:7 ;
hence A . j c= M . j ; :: thesis: verum

end;

end;

end;

then A c= M ;
then reconsider AA = A as ManySortedSubset of M by PBOOLE:def 18;
reconsider a = AA as Element of Bool M by CLOSURE2:def 1;
A11: for j being object st j in I holds
a . j c= x . j

proof

let j be object ; :: thesis: ( j in I implies a . j c= x . j )
assume A12: j in I ; :: thesis: a . j c= x . j

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

suppose A13: i = j ; :: thesis: a . j c= x . j

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in a . j or v in x . j )
assume A14: v in a . j ; :: thesis: v in x . j
a . j = {y} by A3, A4, A13, FUNCT_4:13;
hence v in x . j by A1, A13, A14, TARSKI:def 1; :: thesis: verum

end;

suppose j <> i ; :: thesis: a . j c= x . j

then A15: not j in {i} by TARSKI:def 1;
j in (dom (EmptyMS I)) \/ (dom ({i} --> {y})) by A6, A12, FUNCT_4:def 1;
then a . j = (I --> {}) . j by A2, A15, FUNCT_4:def 1
.= {} by A12, FUNCOP_1:7 ;
hence a . j c= x . j ; :: thesis: verum

end;

end;

end;

A16: { b where b is Element of I : a . b <> {} } = {i}

proof

thus { b where b is Element of I : a . b <> {} } c= {i} :: according to XBOOLE_0:def 10 :: thesis: {i} c= { b where b is Element of I : a . b <> {} }

proof

let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in { b where b is Element of I : a . b <> {} } or s in {i} )
assume s in { b where b is Element of I : a . b <> {} } ; :: thesis: s in {i}
then A17: ex b being Element of I st
( s = b & a . b <> {} ) ;
assume A18: not s in {i} ; :: thesis: contradiction
reconsider s = s as Element of I by A17;
s in dom a by A6;
then s in (dom (EmptyMS I)) \/ (dom ({i} --> {y})) by FUNCT_4:def 1;
then a . s = (I --> {}) . s by A2, A18, FUNCT_4:def 1
.= {} by FUNCOP_1:7 ;
hence contradiction by A17; :: thesis: verum

end;

let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in {i} or s in { b where b is Element of I : a . b <> {} } )
assume A19: s in {i} ; :: thesis: s in { b where b is Element of I : a . b <> {} }
then A20: s = i by TARSKI:def 1;
reconsider s = s as Element of I by A19, TARSKI:def 1;
a . s = {y} by A3, A4, A20, FUNCT_4:13;
hence s in { b where b is Element of I : a . b <> {} } ; :: thesis: verum

end;

take a ; :: thesis: ( y in a . i & a is finite-yielding & support a is finite & a c= x )
for j being object st j in I holds
a . j is finite

proof

let j be object ; :: thesis: ( j in I implies a . j is finite )
assume A21: j in I ; :: thesis: a . j is finite

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

suppose j = i ; :: thesis: a . j is finite

hence a . j is finite by A3, A4, FUNCT_4:13; :: thesis: verum

end;

suppose j <> i ; :: thesis: a . j is finite

then A22: not j in {i} by TARSKI:def 1;
j in (dom (EmptyMS I)) \/ (dom ({i} --> {y})) by A6, A21, FUNCT_4:def 1;
then a . j = (I --> {}) . j by A2, A22, FUNCT_4:def 1
.= {} by A21, FUNCOP_1:7 ;
hence a . j is finite ; :: thesis: verum

end;

end;

end;

hence ( y in a . i & a is finite-yielding & support a is finite & a c= x ) by A5, A16, A11, FINSET_1:def 5, TARSKI:def 1; :: thesis: verum