let I be non empty set ; :: thesis: for i being Element of I
for H being Group-like associative multMagma-Family of I st I is trivial holds
injection (H,i) is bijective
let i be Element of I; :: thesis: for H being Group-like associative multMagma-Family of I st I is trivial holds
injection (H,i) is bijective
let H be Group-like associative multMagma-Family of I; :: thesis: ( I is trivial implies injection (H,i) is bijective )
assume A1: I is trivial ; :: thesis: injection (H,i) is bijective

now :: thesis: for Z being object st Z in the carrier of (FreeProduct H) holds
Z in rng (injection (H,i))

let Z be object ; :: thesis: ( Z in the carrier of (FreeProduct H) implies b₁ in rng (injection (H,i)) )
assume Z in the carrier of (FreeProduct H) ; :: thesis: b₁ in rng (injection (H,i))
then consider p being Element of ((FreeAtoms H) *+^+<0>) such that
A2: Z = Class ((EqCl (ReductionRel H)),p) by EQREL_1:36;
p in the carrier of ((FreeAtoms H) *+^+<0>) ;
then p in (FreeAtoms H) * by MONOID_0:61;
then reconsider p = p as FinSequence of FreeAtoms H by FINSEQ_1:def 11;

per cases ( not p is empty or p is empty ) ;

suppose not p is empty ; :: thesis: b₁ in rng (injection (H,i))

then consider g being Element of (H . i) such that
A3: ReductionRel H reduces p,<*[i,g]*> by A1, Th42;
[i,g] in FreeAtoms H by Th9;
then reconsider s = <*[i,g]*> as FinSequence of FreeAtoms H by FINSEQ_1:74;
s in (FreeAtoms H) * by FINSEQ_1:def 11;
then A4: s in the carrier of ((FreeAtoms H) *+^+<0>) by MONOID_0:61;
dom (injection (H,i)) = the carrier of (H . i) by FUNCT_2:def 1;
then A5: g in dom (injection (H,i)) ;
p,s are_convertible_wrt ReductionRel H by A3, REWRITE1:25;
then [p,s] in EqCl (ReductionRel H) by A4, MSUALG_6:41;
then Z = [*i,g*] by A2, EQREL_1:35
.= (injection (H,i)) . g by Th56 ;
hence Z in rng (injection (H,i)) by A5, FUNCT_1:3; :: thesis: verum

end;

suppose p is empty ; :: thesis: b₁ in rng (injection (H,i))

then A6: Z = 1_ (FreeProduct H) by A2, Th45
.= [*i,(1_ (H . i))*] by Th49
.= (injection (H,i)) . (1_ (H . i)) by Th56 ;
dom (injection (H,i)) = the carrier of (H . i) by FUNCT_2:def 1;
hence Z in rng (injection (H,i)) by A6, FUNCT_1:3; :: thesis: verum

end;

end;

end;

then the carrier of (FreeProduct H) c= rng (injection (H,i)) by TARSKI:def 3;
then injection (H,i) is onto by XBOOLE_0:def 10, FUNCT_2:def 3;
hence injection (H,i) is bijective by FUNCT_2:def 4; :: thesis: verum