let T, U be non empty TopSpace; :: thesis: for t being Point of T
for f being Loop of t
for g being continuous Function of T,U st f is nullhomotopic holds
g * f is nullhomotopic
let t be Point of T; :: thesis: for f being Loop of t
for g being continuous Function of T,U st f is nullhomotopic holds
g * f is nullhomotopic
let f be Loop of t; :: thesis: for g being continuous Function of T,U st f is nullhomotopic holds
g * f is nullhomotopic
let g be continuous Function of T,U; :: thesis: ( f is nullhomotopic implies g * f is nullhomotopic )
given c being constant Loop of t such that A1: f,c are_homotopic ; :: according to TOPALG_6:def 3 :: thesis: g * f is nullhomotopic
consider F being Function of [:I[01],I[01]:],T such that
A2: F is continuous and
A3: for s being Point of I[01] holds
( F . (s,0) = f . s & F . (s,1) = c . s & F . (0,s) = t & F . (1,s) = t ) by A1;
reconsider d = I[01] --> (g . t) as constant Loop of g . t by JORDAN:41;
reconsider G = g * F as Function of [:I[01],I[01]:],U ;
take d ; :: according to TOPALG_6:def 3 :: thesis: g * f,d are_homotopic
take G ; :: according to BORSUK_2:def 7 :: thesis: ( G is continuous & ( for b₁ being Element of the carrier of I[01] holds
( G . (b₁,0) = (g * f) . b₁ & G . (b₁,1) = d . b₁ & G . (0,b₁) = g . t & G . (1,b₁) = g . t ) ) )
thus G is continuous by A2; :: thesis: for b₁ being Element of the carrier of I[01] holds
( G . (b₁,0) = (g * f) . b₁ & G . (b₁,1) = d . b₁ & G . (0,b₁) = g . t & G . (1,b₁) = g . t )
let s be Point of I[01]; :: thesis: ( G . (s,0) = (g * f) . s & G . (s,1) = d . s & G . (0,s) = g . t & G . (1,s) = g . t )
reconsider j0 = 0 , j1 = 1 as Point of I[01] by BORSUK_1:def 14, BORSUK_1:def 15;
set I = the carrier of I[01];
A4: the carrier of [:I[01],I[01]:] = [: the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;
thus G . (s,0) = g . (F . (s,j0)) by A4, BINOP_1:18
.= g . (f . s) by A3
.= (g * f) . s by FUNCT_2:15 ; :: thesis: ( G . (s,1) = d . s & G . (0,s) = g . t & G . (1,s) = g . t )
thus G . (s,1) = g . (F . (s,j1)) by A4, BINOP_1:18
.= g . (c . s) by A3
.= g . t by TOPALG_3:21
.= d . s ; :: thesis: ( G . (0,s) = g . t & G . (1,s) = g . t )
thus G . (0,s) = g . (F . (j0,s)) by A4, BINOP_1:18
.= g . t by A3 ; :: thesis: G . (1,s) = g . t
thus G . (1,s) = g . (F . (j1,s)) by A4, BINOP_1:18
.= g . t by A3 ; :: thesis: verum