set f = id I[01] ;
( (id I[01] ) . 0 = 0[01] & (id I[01] ) . 1 = 1[01] ) by BORSUK_1:def 17, BORSUK_1:def 18, TMAP_1:91;
hence id I[01] is Path of 0[01] , 1[01] by BORSUK_2:def 4; :: thesis: verum