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 V45() & 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 V45() & 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 V45() & 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 V45() & 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 V45() & 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 V45() & support a is finite & a c= x )

set N = {i} --> {y};
set A = () +* ({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 ;
then A5: ((EmptyMS I) +* ({i} --> {y})) . i = {y} by ;
A6: dom (() +* ({i} --> {y})) = (dom ()) \/ (dom ({i} --> {y})) by FUNCT_4:def 1
.= I \/ {i} by
.= I by ZFMISC_1:40 ;
then reconsider A = () +* ({i} --> {y}) as ManySortedSet of I by ;
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 ;
then A9: v in x . j by ;
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 ()) \/ (dom ({i} --> {y})) by ;
then A . j = () . j by
.= {} by ;
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 ;
hence v in x . j by ; :: 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 ()) \/ (dom ({i} --> {y})) by ;
then a . j = () . j by
.= {} by ;
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 ()) \/ (dom ({i} --> {y})) by FUNCT_4:def 1;
then a . s = () . s by
.= {} 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 ;
a . s = {y} by ;
hence s in { b where b is Element of I : a . b <> {} } ; :: thesis: verum
end;
take a ; :: thesis: ( y in a . i & a is V45() & 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 ; :: thesis: verum
end;
suppose j <> i ; :: thesis: a . j is finite
then A22: not j in {i} by TARSKI:def 1;
j in (dom ()) \/ (dom ({i} --> {y})) by ;
then a . j = () . j by
.= {} by ;
hence a . j is finite ; :: thesis: verum
end;
end;
end;
hence ( y in a . i & a is V45() & support a is finite & a c= x ) by ; :: thesis: verum