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) "
let T be TopGroup; :: thesis: for t being Point of T
for f being Loop of t holds (inverse_loop f) . x = (f . x) "
let t be Point of T; :: thesis: for f being Loop of t holds (inverse_loop f) . x = (f . x) "
let f be Loop of t; :: thesis: (inverse_loop f) . x = (f . x) "
thus (inverse_loop f) . x = (inverse_op T) . (f . x) by FUNCT_2:15
.= (f . x) " by GROUP_1:def 6 ; :: thesis: verum