let T be TopStruct ; :: thesis: for P being Subset of T
for F being Subset-Family of T ex f being Function st
( dom f = F & rng f = F | P & ( for x being set st x in F holds
for Q being Subset of T st Q = x holds
f . x = Q /\ P ) )
let P be Subset of T; :: thesis: for F being Subset-Family of T ex f being Function st
( dom f = F & rng f = F | P & ( for x being set st x in F holds
for Q being Subset of T st Q = x holds
f . x = Q /\ P ) )
let F be Subset-Family of T; :: thesis: ex f being Function st
( dom f = F & rng f = F | P & ( for x being set st x in F holds
for Q being Subset of T st Q = x holds
f . x = Q /\ P ) )
defpred S₁[ set , set ] means for Q being Subset of T st Q = $1 holds
$2 = Q /\ P;
A1: for x being set st x in F holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in F implies ex y being set st S₁[x,y] )
assume x in F ; :: thesis: ex y being set st S₁[x,y]
then reconsider Q = x as Subset of T ;
reconsider y = Q /\ P as set ;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

consider f being Function such that
A2: dom f = F and
A3: for x being set st x in F holds
S₁[x,f . x] from CLASSES1:sch 1(A1);
take f ; :: thesis: ( dom f = F & rng f = F | P & ( for x being set st x in F holds
for Q being Subset of T st Q = x holds
f . x = Q /\ P ) )
thus dom f = F by A2; :: thesis: ( rng f = F | P & ( for x being set st x in F holds
for Q being Subset of T st Q = x holds
f . x = Q /\ P ) )
for x being set holds
( x in rng f iff x in F | P )

proof

let x be set ; :: thesis: ( x in rng f iff x in F | P )

hereby :: thesis: ( x in F | P implies x in rng f )

assume x in rng f ; :: thesis: x in F | P
then consider y being set such that
A4: y in dom f and
A5: f . y = x by FUNCT_1:def 3;
reconsider Y = y as Subset of T by A2, A4;
Y /\ P c= P by XBOOLE_1:17;
then Y /\ P c= [#] (T | P) by PRE_TOPC:def 5;
then reconsider X = x as Subset of (T | P) by A2, A3, A4, A5;
X = Y /\ P by A2, A3, A4, A5;
hence x in F | P by A2, A4, Def3; :: thesis: verum

end;

assume A6: x in F | P ; :: thesis: x in rng f
then reconsider X = x as Subset of (T | P) ;
consider Q being Subset of T such that
A7: Q in F and
A8: Q /\ P = X by A6, Def3;
reconsider p = Q as set ;
f . p = x by A3, A7, A8;
hence x in rng f by A2, A7, FUNCT_1:def 3; :: thesis: verum

end;

hence rng f = F | P by TARSKI:1; :: thesis: for x being set st x in F holds
for Q being Subset of T st Q = x holds
f . x = Q /\ P
thus for x being set st x in F holds
for Q being Subset of T st Q = x holds
f . x = Q /\ P by A3; :: thesis: verum