let T be non empty TopSpace; :: thesis: for T0 being T_0-TopSpace
for f being continuous Function of T,T0
for p being Point of T holds f .: (Class ((),p)) = {(f . p)}

let T0 be T_0-TopSpace; :: thesis: for f being continuous Function of T,T0
for p being Point of T holds f .: (Class ((),p)) = {(f . p)}

let f be continuous Function of T,T0; :: thesis: for p being Point of T holds f .: (Class ((),p)) = {(f . p)}
let p be Point of T; :: thesis: f .: (Class ((),p)) = {(f . p)}
set R = Indiscernibility T;
for y being object holds
( y in f .: (Class ((),p)) iff y in {(f . p)} )
proof
let y be object ; :: thesis: ( y in f .: (Class ((),p)) iff y in {(f . p)} )
hereby :: thesis: ( y in {(f . p)} implies y in f .: (Class ((),p)) )
assume y in f .: (Class ((),p)) ; :: thesis: y in {(f . p)}
then consider x being object such that
A1: x in the carrier of T and
A2: x in Class ((),p) and
A3: y = f . x by FUNCT_2:64;
[x,p] in Indiscernibility T by ;
then f . x = f . p by ;
hence y in {(f . p)} by ; :: thesis: verum
end;
assume y in {(f . p)} ; :: thesis: y in f .: (Class ((),p))
then A4: y = f . p by TARSKI:def 1;
p in Class ((),p) by EQREL_1:20;
hence y in f .: (Class ((),p)) by ; :: thesis: verum
end;
hence f .: (Class ((),p)) = {(f . p)} by TARSKI:2; :: thesis: verum