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) st g <> 1_ (H . i) holds
factorization [*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) st g <> 1_ (H . i) holds
factorization [*i,g*] = <*[*i,g*]*>
let H be Group-like associative multMagma-Family of I; :: thesis: for g being Element of (H . i) st g <> 1_ (H . i) holds
factorization [*i,g*] = <*[*i,g*]*>
let g be Element of (H . i); :: thesis: ( g <> 1_ (H . i) implies factorization [*i,g*] = <*[*i,g*]*> )
assume A1: g <> 1_ (H . i) ; :: thesis: factorization [*i,g*] = <*[*i,g*]*>
A2: ( [i,g] in dom (uncurry (injection H)) & (uncurry (injection H)) . [i,g] = [*i,g*] )

proof

i in I ;
then A3: i in dom (injection H) by PARTFUN1:def 2;
A4: injection (H,i) = (injection H) . i by Def9;
A5: dom (injection (H,i)) = the carrier of (H . i) by FUNCT_2:def 1;
A6: [i,g] in FreeAtoms H by Th9;
uncurry (injection H) is ManySortedSet of FreeAtoms H by Lm5;
hence [i,g] in dom (uncurry (injection H)) by A6, PARTFUN1:def 2; :: thesis: (uncurry (injection H)) . [i,g] = [*i,g*]
thus (uncurry (injection H)) . [i,g] = (uncurry (injection H)) . (i,g) by BINOP_1:def 1
.= (injection (H,i)) . g by A3, A4, A5, FUNCT_5:38
.= [*i,g*] by Th56 ; :: thesis: verum

end;

thus factorization [*i,g*] = (uncurry (injection H)) * <*[i,g]*> by A1, Th64
.= <*[*i,g*]*> by A2, FINSEQ_2:34 ; :: thesis: verum