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

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

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

dom (I[01] --> a) = the carrier of I[01]
by FUNCT_2:def 1;
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;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

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