let T be non empty TopSpace; :: thesis: for t being Point of T
for x being Point of I[01]
for P being constant Loop of t holds P . x = t
let t be Point of T; :: thesis: for x being Point of I[01]
for P being constant Loop of t holds P . x = t
let x be Point of I[01]; :: thesis: for P being constant Loop of t holds P . x = t
let P be constant Loop of t; :: thesis: P . x = t
P = I[01] --> t by BORSUK_2:5;
hence P . x = t ; :: thesis: verum