let S be non empty pathwise_connected TopSpace; 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; 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; 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; for P being Path of a,b holds f * P is Path of f . a,f . b
let P be Path of a,b; 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; verum