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 = (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

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

for j being object st j in I holds

a . j is finite

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 = (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

then
A c= M
;
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

end;assume A7: j in I ; :: thesis: A . j c= M . j

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

end;

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;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

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

A16:
{ b where b is Element of I : a . b <> {} } = {i}
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

end;assume A12: j in I ; :: thesis: a . j c= x . j

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

end;

proof

take
a
; :: thesis: ( y in a . i & a is V45() & support a is finite & a c= x )
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 <> {} }

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;proof

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 <> {} } )
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;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

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

for j being object st j in I holds

a . j is finite

proof

hence
( y in a . i & a is V45() & support a is finite & a c= x )
by A5, A16, A11, FINSET_1:def 5, TARSKI:def 1; :: thesis: verum
let j be object ; :: thesis: ( j in I implies a . j is finite )

assume A21: j in I ; :: thesis: a . j is finite

end;assume A21: j in I ; :: thesis: a . j is finite