let T be non empty TopSpace; :: thesis: for t being Point of T

for S being non empty SubSpace of T

for s being Point of S

for f being Loop of t

for g being Loop of s st t = s & f = g & g is nullhomotopic holds

f is nullhomotopic

let t be Point of T; :: thesis: for S being non empty SubSpace of T

for s being Point of S

for f being Loop of t

for g being Loop of s st t = s & f = g & g is nullhomotopic holds

f is nullhomotopic

let S be non empty SubSpace of T; :: thesis: for s being Point of S

for f being Loop of t

for g being Loop of s st t = s & f = g & g is nullhomotopic holds

f is nullhomotopic

let s be Point of S; :: thesis: for f being Loop of t

for g being Loop of s st t = s & f = g & g is nullhomotopic holds

f is nullhomotopic

let f be Loop of t; :: thesis: for g being Loop of s st t = s & f = g & g is nullhomotopic holds

f is nullhomotopic

let g be Loop of s; :: thesis: ( t = s & f = g & g is nullhomotopic implies f is nullhomotopic )

assume that

A1: ( t = s & f = g ) and

A2: g is nullhomotopic ; :: thesis: f is nullhomotopic

consider c being constant Loop of s such that

A3: g,c are_homotopic by A2;

c = I[01] --> s by BORSUK_2:5

.= I[01] --> t by A1 ;

then reconsider c = c as constant Loop of t by JORDAN:41;

f,c are_homotopic by A1, A3, Th6;

hence f is nullhomotopic ; :: thesis: verum

for S being non empty SubSpace of T

for s being Point of S

for f being Loop of t

for g being Loop of s st t = s & f = g & g is nullhomotopic holds

f is nullhomotopic

let t be Point of T; :: thesis: for S being non empty SubSpace of T

for s being Point of S

for f being Loop of t

for g being Loop of s st t = s & f = g & g is nullhomotopic holds

f is nullhomotopic

let S be non empty SubSpace of T; :: thesis: for s being Point of S

for f being Loop of t

for g being Loop of s st t = s & f = g & g is nullhomotopic holds

f is nullhomotopic

let s be Point of S; :: thesis: for f being Loop of t

for g being Loop of s st t = s & f = g & g is nullhomotopic holds

f is nullhomotopic

let f be Loop of t; :: thesis: for g being Loop of s st t = s & f = g & g is nullhomotopic holds

f is nullhomotopic

let g be Loop of s; :: thesis: ( t = s & f = g & g is nullhomotopic implies f is nullhomotopic )

assume that

A1: ( t = s & f = g ) and

A2: g is nullhomotopic ; :: thesis: f is nullhomotopic

consider c being constant Loop of s such that

A3: g,c are_homotopic by A2;

c = I[01] --> s by BORSUK_2:5

.= I[01] --> t by A1 ;

then reconsider c = c as constant Loop of t by JORDAN:41;

f,c are_homotopic by A1, A3, Th6;

hence f is nullhomotopic ; :: thesis: verum