let i, I be set ; :: thesis: for f being Function
for F being Group-like multMagma-Family of I
for G being non empty Group-like multMagma st i in I & G = F . i & f = 1_ () holds
f . i = 1_ G

let f be Function; :: thesis: for F being Group-like multMagma-Family of I
for G being non empty Group-like multMagma st i in I & G = F . i & f = 1_ () holds
f . i = 1_ G

let F be Group-like multMagma-Family of I; :: thesis: for G being non empty Group-like multMagma st i in I & G = F . i & f = 1_ () holds
f . i = 1_ G

let G be non empty Group-like multMagma ; :: thesis: ( i in I & G = F . i & f = 1_ () implies f . i = 1_ G )
assume that
A1: i in I and
A2: G = F . i and
A3: f = 1_ () ; :: thesis: f . i = 1_ G
set GP = product F;
f in the carrier of () by A3;
then A4: f in product () by Def2;
then reconsider e = f . i as Element of G by A1, A2, Lm1;
now :: thesis: for h being Element of G holds
( h * e = h & e * h = h )
let h be Element of G; :: thesis: ( h * e = h & e * h = h )
defpred S1[ object , object ] means ( ( \$1 = i implies \$2 = h ) & ( \$1 <> i implies ex H being non empty Group-like multMagma st
( H = F . \$1 & \$2 = 1_ H ) ) );
A5: for j being object st j in I holds
ex k being object st S1[j,k]
proof
let j be object ; :: thesis: ( j in I implies ex k being object st S1[j,k] )
assume A6: j in I ; :: thesis: ex k being object st S1[j,k]
per cases ( j = i or j <> i ) ;
suppose j = i ; :: thesis: ex k being object st S1[j,k]
hence ex k being object st S1[j,k] ; :: thesis: verum
end;
suppose A7: j <> i ; :: thesis: ex k being object st S1[j,k]
consider Fj being non empty Group-like multMagma such that
A8: Fj = F . j by ;
take 1_ Fj ; :: thesis: S1[j, 1_ Fj]
thus ( j = i implies 1_ Fj = h ) by A7; :: thesis: ( j <> i implies ex H being non empty Group-like multMagma st
( H = F . j & 1_ Fj = 1_ H ) )

thus ( j <> i implies ex H being non empty Group-like multMagma st
( H = F . j & 1_ Fj = 1_ H ) ) by A8; :: thesis: verum
end;
end;
end;
consider g being ManySortedSet of I such that
A9: for j being object st j in I holds
S1[j,g . j] from A10: dom g = I by PARTFUN1:def 2;
A11: now :: thesis: for j being object st j in dom g holds
g . j in () . j
let j be object ; :: thesis: ( j in dom g implies g . b1 in () . b1 )
assume A12: j in dom g ; :: thesis: g . b1 in () . b1
then A13: ex R being 1-sorted st
( R = F . j & () . j = the carrier of R ) by PRALG_1:def 13;
per cases ( i = j or j <> i ) ;
suppose A14: i = j ; :: thesis: g . b1 in () . b1
then g . j = h by ;
hence g . j in () . j by A2, A13, A14; :: thesis: verum
end;
suppose j <> i ; :: thesis: g . b1 in () . b1
then ex H being non empty Group-like multMagma st
( H = F . j & g . j = 1_ H ) by ;
hence g . j in () . j by A13; :: thesis: verum
end;
end;
end;
dom () = I by PARTFUN1:def 2;
then A15: g in product () by ;
then reconsider g1 = g as Element of () by Def2;
A16: g1 * (1_ ()) = g1 by GROUP_1:def 4;
A17: g . i = h by A1, A9;
A18: g . i = h by A1, A9;
ex Fi being non empty multMagma ex m being Function st
( Fi = F . i & m = the multF of () . (g,f) & m . i = the multF of Fi . ((g . i),(f . i)) ) by A1, A4, A15, Def2;
hence h * e = h by A2, A3, A16, A18; :: thesis: e * h = h
A19: (1_ ()) * g1 = g1 by GROUP_1:def 4;
ex Fi being non empty multMagma ex m being Function st
( Fi = F . i & m = the multF of () . (f,g) & m . i = the multF of Fi . ((f . i),(g . i)) ) by A1, A4, A15, Def2;
hence e * h = h by A2, A3, A19, A17; :: thesis: verum
end;
hence f . i = 1_ G by GROUP_1:4; :: thesis: verum