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