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:
consider c being constant Loop of s such that
A3: g,c are_homotopic by A2;
c = I --> s by BORSUK_2:5
.= I --> 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