let I be set ; :: thesis: for M being ManySortedSet of I
for X being Element of bool M
for i, x being set st i in I & x in ((id (bool M)) .. X) . i holds
ex Y being V30() Element of bool M st
( Y c= X & x in ((id (bool M)) .. Y) . i )
let M be ManySortedSet of I; :: thesis: for X being Element of bool M
for i, x being set st i in I & x in ((id (bool M)) .. X) . i holds
ex Y being V30() Element of bool M st
( Y c= X & x in ((id (bool M)) .. Y) . i )
let X be Element of bool M; :: thesis: for i, x being set st i in I & x in ((id (bool M)) .. X) . i holds
ex Y being V30() Element of bool M st
( Y c= X & x in ((id (bool M)) .. Y) . i )
let i, x be set ; :: thesis: ( i in I & x in ((id (bool M)) .. X) . i implies ex Y being V30() Element of bool M st
( Y c= X & x in ((id (bool M)) .. Y) . i ) )
assume that
A1: i in I and
A2: x in ((id (bool M)) .. X) . i ; :: thesis: ex Y being V30() Element of bool M st
( Y c= X & x in ((id (bool M)) .. Y) . i )
A3: x in X . i by A2, Th8;
set Y = (I --> {}) +* (i .--> {x});
dom ((I --> {}) +* (i .--> {x})) = I by A1, PZFMISC1:1;
then reconsider Y = (I --> {}) +* (i .--> {x}) as ManySortedSet of I by PARTFUN1:def 4, RELAT_1:def 18;
A4: dom (i .--> {x}) = {i} by FUNCOP_1:19;
i in {i} by TARSKI:def 1;
then A5: Y . i = (i .--> {x}) . i by A4, FUNCT_4:14
.= {x} by FUNCOP_1:87 ;
X in bool M by MSSUBFAM:12;
then X c= M by MBOOLEAN:19;
then A6: X . i c= M . i by A1, PBOOLE:def 5;
Y is Element of bool M

proof

let j be set ; :: according to PBOOLE:def 17 :: thesis: ( not j in I or Y . j is Element of (bool M) . j )
assume A7: j in I ; :: thesis: Y . j is Element of (bool M) . j

now

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

case A8: j = i ; :: thesis: Y . j is Element of (bool M) . j

then {x} c= M . j by A3, A6, ZFMISC_1:37;
hence Y . j is Element of (bool M) . j by A5, A7, A8, MBOOLEAN:def 1; :: thesis: verum

end;

case j <> i ; :: thesis: Y . j is Element of (bool M) . j

then not j in dom (i .--> {x}) by A4, TARSKI:def 1;
then Y . j = (I --> {}) . j by FUNCT_4:12;
then Y . j = {} by A7, FUNCOP_1:13;
then Y . j c= M . j by XBOOLE_1:2;
hence Y . j is Element of (bool M) . j by A7, MBOOLEAN:def 1; :: thesis: verum

end;

end;

end;

hence Y . j is Element of (bool M) . j ; :: thesis: verum

end;

then reconsider Y = Y as Element of bool M ;
Y is finite-yielding

proof

let j be set ; :: according to FINSET_1:def 4 :: thesis: ( not j in I or Y . j is finite )
assume A9: j in I ; :: thesis: Y . j is finite

now

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

case j = i ; :: thesis: Y . j is finite

hence Y . j is finite by A5; :: thesis: verum

end;

case j <> i ; :: thesis: Y . j is finite

then not j in dom (i .--> {x}) by A4, TARSKI:def 1;
then Y . j = (I --> {}) . j by FUNCT_4:12;
hence Y . j is finite by A9, FUNCOP_1:13; :: thesis: verum

end;

end;

end;

hence Y . j is finite ; :: thesis: verum

end;

then reconsider Y = Y as V30() Element of bool M ;
take Y ; :: thesis: ( Y c= X & x in ((id (bool M)) .. Y) . i )
thus Y c= X :: thesis: x in ((id (bool M)) .. Y) . i

proof

let j be set ; :: according to PBOOLE:def 5 :: thesis: ( not j in I or Y . j c= X . j )
assume A10: j in I ; :: thesis: Y . j c= X . j

now

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

case j = i ; :: thesis: Y . j c= X . j

hence Y . j c= X . j by A3, A5, ZFMISC_1:37; :: thesis: verum

end;

case j <> i ; :: thesis: Y . j c= X . j

then not j in dom (i .--> {x}) by A4, TARSKI:def 1;
then Y . j = (I --> {}) . j by FUNCT_4:12;
then Y . j = {} by A10, FUNCOP_1:13;
hence Y . j c= X . j by XBOOLE_1:2; :: thesis: verum

end;

end;

end;

hence Y . j c= X . j ; :: thesis: verum

end;

x in Y . i by A5, TARSKI:def 1;
hence x in ((id (bool M)) .. Y) . i by Th8; :: thesis: verum