let S, T be non empty TopSpace; :: thesis: for f being continuous Function of S,T
for a being Point of S
for P being Loop of a holds f * P is Loop of f . a
let f be continuous Function of S,T; :: thesis: for a being Point of S
for P being Loop of a holds f * P is Loop of f . a
let a be Point of S; :: thesis: for P being Loop of a holds f * P is Loop of f . a
let P be Loop of a; :: thesis: f * P is Loop of f . a
A1: f . a,f . a are_connected ;
A2: (f * P) . 1 = f . (P . j1) by FUNCT_2:15
.= f . a by Th22 ;
(f * P) . 0 = f . (P . j0) by FUNCT_2:15
.= f . a by Th22 ;
hence f * P is Loop of f . a by A2, A1, BORSUK_2:def 2; :: thesis: verum