let S be non empty pathwise_connected TopSpace; :: thesis: for T being non empty TopSpace

for f being continuous Function of S,T

for a, b being Point of S

for P being Path of a,b holds f * P is Path of f . a,f . b

let 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 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 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 holds f * P is Path of f . a,f . b

let P be Path of a,b; :: thesis: f * P is Path of f . a,f . b

A1: a,b are_connected by BORSUK_2:def 3;

A2: (f * P) . 1 = f . (P . j1) by FUNCT_2:15

.= f . b by A1, BORSUK_2:def 2 ;

A3: (f * P) . 0 = f . (P . j0) by FUNCT_2:15

.= f . a by A1, BORSUK_2:def 2 ;

f . a,f . b are_connected by A1, Th23;

hence f * P is Path of f . a,f . b by A3, A2, BORSUK_2:def 2; :: thesis: verum

for f being continuous Function of S,T

for a, b being Point of S

for P being Path of a,b holds f * P is Path of f . a,f . b

let 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 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 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 holds f * P is Path of f . a,f . b

let P be Path of a,b; :: thesis: f * P is Path of f . a,f . b

A1: a,b are_connected by BORSUK_2:def 3;

A2: (f * P) . 1 = f . (P . j1) by FUNCT_2:15

.= f . b by A1, BORSUK_2:def 2 ;

A3: (f * P) . 0 = f . (P . j0) by FUNCT_2:15

.= f . a by A1, BORSUK_2:def 2 ;

f . a,f . b are_connected by A1, Th23;

hence f * P is Path of f . a,f . b by A3, A2, BORSUK_2:def 2; :: thesis: verum