let T be non empty TopSpace; :: thesis: for a, b being Point of T
for f being Path of a,b st a,b are_connected holds
rng f c= rng (- f)
let a, b be Point of T; :: thesis: for f being Path of a,b st a,b are_connected holds
rng f c= rng (- f)
let f be Path of a,b; :: thesis: ( a,b are_connected implies rng f c= rng (- f) )
assume A1: a,b are_connected ; :: thesis: rng f c= rng (- f)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in rng (- f) )
assume y in rng f ; :: thesis: y in rng (- f)
then consider x being object such that
A2: x in dom f and
A3: f . x = y by FUNCT_1:def 3;
reconsider x = x as Point of I[01] by A2;
A4: dom (- f) = the carrier of I[01] by FUNCT_2:def 1;
A5: 1 - x is Point of I[01] by JORDAN5B:4;
then (- f) . (1 - x) = f . (1 - (1 - x)) by A1, BORSUK_2:def 6;
hence y in rng (- f) by A3, A4, A5, FUNCT_1:def 3; :: thesis: verum