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 ((Indiscernibility T),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 ((Indiscernibility T),p)) = {(f . p)}
let f be continuous Function of T,T0; :: thesis: for p being Point of T holds f .: (Class ((Indiscernibility T),p)) = {(f . p)}
let p be Point of T; :: thesis: f .: (Class ((Indiscernibility T),p)) = {(f . p)}
set R = Indiscernibility T;
for y being object holds
( y in f .: (Class ((Indiscernibility T),p)) iff y in {(f . p)} )

proof

let y be object ; :: thesis: ( y in f .: (Class ((Indiscernibility T),p)) iff y in {(f . p)} )

hereby :: thesis: ( y in {(f . p)} implies y in f .: (Class ((Indiscernibility T),p)) )

assume y in f .: (Class ((Indiscernibility T),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 ((Indiscernibility T),p) and
A3: y = f . x by FUNCT_2:64;
[x,p] in Indiscernibility T by A2, EQREL_1:19;
then f . x = f . p by A1, Th11;
hence y in {(f . p)} by A3, TARSKI:def 1; :: thesis: verum

end;

assume y in {(f . p)} ; :: thesis: y in f .: (Class ((Indiscernibility T),p))
then A4: y = f . p by TARSKI:def 1;
p in Class ((Indiscernibility T),p) by EQREL_1:20;
hence y in f .: (Class ((Indiscernibility T),p)) by A4, FUNCT_2:35; :: thesis: verum

end;

hence f .: (Class ((Indiscernibility T),p)) = {(f . p)} by TARSKI:2; :: thesis: verum