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, Def3;
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 by Def3; :: thesis: verum