let x be Point of I[01]; :: thesis: for T being TopGroup

for t being Point of T

for f being Loop of t holds (f . x) * ((inverse_loop f) . x) = 1_ T

let T be TopGroup; :: thesis: for t being Point of T

for f being Loop of t holds (f . x) * ((inverse_loop f) . x) = 1_ T

let t be Point of T; :: thesis: for f being Loop of t holds (f . x) * ((inverse_loop f) . x) = 1_ T

let f be Loop of t; :: thesis: (f . x) * ((inverse_loop f) . x) = 1_ T

(inverse_loop f) . x = (f . x) " by Th2;

hence (f . x) * ((inverse_loop f) . x) = 1_ T by GROUP_1:def 5; :: thesis: verum

for t being Point of T

for f being Loop of t holds (f . x) * ((inverse_loop f) . x) = 1_ T

let T be TopGroup; :: thesis: for t being Point of T

for f being Loop of t holds (f . x) * ((inverse_loop f) . x) = 1_ T

let t be Point of T; :: thesis: for f being Loop of t holds (f . x) * ((inverse_loop f) . x) = 1_ T

let f be Loop of t; :: thesis: (f . x) * ((inverse_loop f) . x) = 1_ T

(inverse_loop f) . x = (f . x) " by Th2;

hence (f . x) * ((inverse_loop f) . x) = 1_ T by GROUP_1:def 5; :: thesis: verum