set PF = P * f;
0 in the carrier of I[01] by BORSUK_1:43;
then 0 in dom f by FUNCT_2:def 1;
then A4: (P * f) . 0 = P . (f . 0) by FUNCT_1:13
.= a by A1, A3, BORSUK_2:def 2 ;
1 in the carrier of I[01] by BORSUK_1:43;
then 1 in dom f by FUNCT_2:def 1;
then A5: (P * f) . 1 = P . (f . 1) by FUNCT_1:13
.= b by A2, A3, BORSUK_2:def 2 ;
P is continuous by A3, BORSUK_2:def 2;
hence P * f is Path of a,b by A3, A4, A5, BORSUK_2:def 2; :: thesis: verum