let T be TopStruct ; :: thesis:
let P be Subset of T; :: thesis:
let F be Subset-Family of T; :: thesis:
defpred S₁[ object , object ] means for Q being Subset of T st Q = $1 holds
$2 = Q /\ P;
A1: for x being object st x in F holds
ex y being object st S₁[x,y]

let x be object ; :: thesis:
assume x in F ; :: thesis:
then reconsider Q = x as Subset of T ;
reconsider y = Q /\ P as set ;
take y ; :: thesis:
thus S₁[x,y] ; :: thesis:

end;

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

let x be object ; :: thesis:

assume x in rng f ; :: thesis:
then consider y being object 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:

end;

assume A6: x in F | P ; :: thesis:
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:

end;

hence rng f = F | P by TARSKI:2; :: thesis:
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: