assume A1: for X being ManySortedSet of F1() holds
( X in F2() iff ( X in F3() & P1[X] ) ) ; :: thesis: F2() c= F3()
consider K being ManySortedSet of F1() such that
A2: K in F2() by PBOOLE:134;
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in F1() or F2() . i c= F3() . i )
assume A3: i in F1() ; :: thesis: F2() . i c= F3() . i
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F2() . i or x in F3() . i )
assume A4: x in F2() . i ; :: thesis: x in F3() . i
dom (K +* (i .--> x)) = F1() by A3, PZFMISC1:1;
then reconsider X = K +* (i .--> x) as ManySortedSet of F1() by PARTFUN1:def 2, RELAT_1:def 18;
A5: dom (i .--> x) = {i} ;
i in {i} by TARSKI:def 1;
then A6: X . i = (i .--> x) . i by A5, FUNCT_4:13
.= x by FUNCOP_1:72 ;
X in F2()
proof
let s be object ; :: according to PBOOLE:def 1 :: thesis: ( not s in F1() or X . s in F2() . s )
assume A7: s in F1() ; :: thesis: X . s in F2() . s
per cases ( s = i or s <> i ) ;
suppose s = i ; :: thesis: X . s in F2() . s
hence X . s in F2() . s by A4, A6; :: thesis: verum
end;
suppose s <> i ; :: thesis: X . s in F2() . s
then not s in dom (i .--> x) by TARSKI:def 1;
then X . s = K . s by FUNCT_4:11;
hence X . s in F2() . s by A2, A7; :: thesis: verum
end;
end;
end;
then X in F3() by A1;
hence x in F3() . i by A3, A6; :: thesis: verum