let S, T be non empty TopSpace; :: thesis: for f being continuous Function of S,T
for a, b being Point of S
for P being Path of a,b st a,b are_connected holds
f * P is Path of f . a,f . b
let f be continuous Function of S,T; :: thesis: for a, b being Point of S
for P being Path of a,b st a,b are_connected holds
f * P is Path of f . a,f . b
let a, b be Point of S; :: thesis: for P being Path of a,b st a,b are_connected holds
f * P is Path of f . a,f . b
let P be Path of a,b; :: thesis: ( a,b are_connected implies f * P is Path of f . a,f . b )
assume A1: a,b are_connected ; :: thesis: f * P is Path of f . a,f . b
then P is continuous by BORSUK_2:def 2;
then A2: f * P is continuous ;
A3: (f * P) . 0 = f . (P . j0) by FUNCT_2:21
.= f . a by A1, BORSUK_2:def 2 ;
A4: (f * P) . 1 = f . (P . j1) by FUNCT_2:21
.= f . b by A1, BORSUK_2:def 2 ;
f . a,f . b are_connected by A1, Th24;
hence f * P is Path of f . a,f . b by A2, A3, A4, BORSUK_2:def 2; :: thesis: verum