let T be non empty TopSpace; :: thesis: for t being Point of
for x being Point of
for P being constant Loop of t holds P . x = t
let t be Point of ; :: thesis: for x being Point of
for P being constant Loop of t holds P . x = t
let x be Point of ; :: 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:6;
hence P . x = t by FUNCOP_1:13; :: thesis: verum