now :: thesis: ( f - r is continuous & (f - r) . 0 = s - r & (f - r) . 1 = t - r )
thus f - r is continuous ; :: thesis: ( (f - r) . 0 = s - r & (f - r) . 1 = t - r )
thus (f - r) . 0 = (f . j0) - r by VALUED_1:2
.= s - r by BORSUK_2:def 4 ; :: thesis: (f - r) . 1 = t - r
thus (f - r) . 1 = (f . j1) - r by VALUED_1:2
.= t - r by BORSUK_2:def 4 ; :: thesis: verum
end;
hence f - r is Path of s - r,t - r by BORSUK_2:def 4; :: thesis: verum