let I be non empty set ; :: thesis: for i being Element of I
for H being Group-like associative multMagma-Family of I
for g being Element of (H . i) holds (injection (H,i)) . g = [*i,g*]
let i be Element of I; :: thesis: for H being Group-like associative multMagma-Family of I
for g being Element of (H . i) holds (injection (H,i)) . g = [*i,g*]
let H be Group-like associative multMagma-Family of I; :: thesis: for g being Element of (H . i) holds (injection (H,i)) . g = [*i,g*]
let g be Element of (H . i); :: thesis: (injection (H,i)) . g = [*i,g*]
set C = the carrier of (H . i);
A1: <*[i,g]*> in [*i,g*] by Th48;
dom (commute <*<:( the carrier of (H . i) --> i),(id the carrier of (H . i)):>*>) = the carrier of (H . i) by Th53;
hence (injection (H,i)) . g = (proj (Class (EqCl (ReductionRel H)))) . ((commute <*<:( the carrier of (H . i) --> i),(id the carrier of (H . i)):>*>) . g) by FUNCT_1:13
.= (proj (Class (EqCl (ReductionRel H)))) . <*[i,g]*> by Th54
.= [*i,g*] by A1, EQREL_1:65 ;
:: thesis: verum