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 (uncurry (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 (uncurry (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 (uncurry (injection H)) . [i,g] = [*i,g*]
let g be Element of (H . i); :: thesis: (uncurry (injection H)) . [i,g] = [*i,g*]
A1: dom (injection H) = I by PARTFUN1:def 2;
(injection H) . i = injection (H,i) by Def9;
then A2: dom ((injection H) . i) = the carrier of (H . i) by FUNCT_2:def 1;
thus (uncurry (injection H)) . [i,g] = (uncurry (injection H)) . (i,g) by BINOP_1:def 1
.= ((injection H) . i) . g by A1, A2, FUNCT_5:38
.= (injection (H,i)) . g by Def9
.= [*i,g*] by Th56 ; :: thesis: verum