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 r + f is Path of s + r,t + r by BORSUK_2:def 4; :: thesis: verum