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

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