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

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