:: deftheorem defines injection GR_FREE0:def 6 :
for I being non empty set
for H being Group-like associative multMagma-Family of I
for i being Element of I holds injection (H,i) = (proj (Class (EqCl (ReductionRel H)))) * (commute <*<:( the carrier of (H . i) --> i),(id the carrier of (H . i)):>*>);