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

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