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)} )

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

hence
f .: (Class ((Indiscernibility T),p)) = {(f . p)}
by TARSKI:2; :: thesis: verum
let y be object ; :: thesis: ( y in f .: (Class ((Indiscernibility T),p)) iff y in {(f . 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;hereby :: thesis: ( y in {(f . p)} implies y in f .: (Class ((Indiscernibility T),p)) )

assume
y in {(f . p)}
; :: thesis: 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;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

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