let T be non empty TopSpace; :: thesis: for T0 being T_0-TopSpace
for f being continuous Function of T,T0
for p, q being Point of T st [p,q] in Indiscernibility T holds
f . p = f . q
let T0 be T_0-TopSpace; :: thesis: for f being continuous Function of T,T0
for p, q being Point of T st [p,q] in Indiscernibility T holds
f . p = f . q
let f be continuous Function of T,T0; :: thesis: for p, q being Point of T st [p,q] in Indiscernibility T holds
f . p = f . q
let p, q be Point of T; :: thesis: ( [p,q] in Indiscernibility T implies f . p = f . q )
set p9 = f . p;
set q9 = f . q;
assume that
A1: [p,q] in Indiscernibility T and
A2: not f . p = f . q ; :: thesis: contradiction
consider V being Subset of T0 such that
A3: V is open and
A4: ( ( f . p in V & not f . q in V ) or ( f . q in V & not f . p in V ) ) by A2, Def7;
set A = f " V;
[#] T0 <> {} ;
then A5: f " V is open by A3, TOPS_2:43;
reconsider f = f as Function of the carrier of T, the carrier of T0 ;
q in the carrier of T ;
then A6: q in dom f by FUNCT_2:def 1;
p in the carrier of T ;
then p in dom f by FUNCT_2:def 1;
then ( ( p in f " V & not q in f " V ) or ( q in f " V & not p in f " V ) ) by A4, A6, FUNCT_1:def 7;
hence contradiction by A1, A5, Def3; :: thesis: verum