let T be non empty TopSpace; :: thesis: for a being Point of T
for P being constant Path of a,a holds P = I[01] --> a
let a be Point of T; :: thesis: for P being constant Path of a,a holds P = I[01] --> a
let P be constant Path of a,a; :: thesis: P = I[01] --> a
set IT = I[01] --> a;
A1: dom (I[01] --> a) = the carrier of I[01] by FUNCT_2:def 1;
A2: dom P = the carrier of I[01] by FUNCT_2:def 1;
A3: a,a are_connected ;
for x being set st x in the carrier of I[01] holds
P . x = (I[01] --> a) . x

proof

let x be set ; :: thesis: ( x in the carrier of I[01] implies P . x = (I[01] --> a) . x )
assume A4: x in the carrier of I[01] ; :: thesis: P . x = (I[01] --> a) . x
A5: P . 0 = a by A3, Def2;
0 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then 0 in the carrier of I[01] by BORSUK_1:83, RCOMP_1:def 1;
then P . x = a by A2, A4, A5, FUNCT_1:def 16
.= (I[01] --> a) . x by A4, FUNCOP_1:13 ;
hence P . x = (I[01] --> a) . x ; :: thesis: verum

end;

hence P = I[01] --> a by A1, A2, FUNCT_1:9; :: thesis: verum