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 ((inverse_loop f) . x) * (f . x) = 1_ T
let T be TopGroup; :: thesis: for t being Point of T
for f being Loop of t holds ((inverse_loop f) . x) * (f . x) = 1_ T
let t be Point of T; :: thesis: for f being Loop of t holds ((inverse_loop f) . x) * (f . x) = 1_ T
let f be Loop of t; :: thesis: ((inverse_loop f) . x) * (f . x) = 1_ T
(inverse_loop f) . x = (f . x) " by Th2;
hence ((inverse_loop f) . x) * (f . x) = 1_ T by GROUP_1:def 5; :: thesis: verum