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 P = the carrier of I[01] by FUNCT_2:def 1;
A2: a,a are_connected ;
A3: for x being object st x in the carrier of I[01] holds
P . x = (I[01] --> a) . x
proof
0 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then A4: 0 in the carrier of I[01] by BORSUK_1:40, RCOMP_1:def 1;
let x be object ; :: thesis: ( x in the carrier of I[01] implies P . x = (I[01] --> a) . x )
assume A5: x in the carrier of I[01] ; :: thesis: P . x = (I[01] --> a) . x
P . 0 = a by A2, Def2;
then P . x = a by A1, A5, A4, FUNCT_1:def 10
.= (I[01] --> a) . x by A5, FUNCOP_1:7 ;
hence P . x = (I[01] --> a) . x ; :: thesis: verum
end;
dom (I[01] --> a) = the carrier of I[01] by FUNCT_2:def 1;
hence P = I[01] --> a by A1, A3, FUNCT_1:2; :: thesis: verum