let I, i be set ; :: thesis: for f being Function
for F being Group-like multMagma-Family of
for G being non empty Group-like multMagma st i in I & G = F . i & f = 1_ (product F) holds
f . i = 1_ G
let f be Function; :: thesis: for F being Group-like multMagma-Family of
for G being non empty Group-like multMagma st i in I & G = F . i & f = 1_ (product F) holds
f . i = 1_ G
let F be Group-like multMagma-Family of ; :: thesis: for G being non empty Group-like multMagma st i in I & G = F . i & f = 1_ (product F) holds
f . i = 1_ G
let G be non empty Group-like multMagma ; :: thesis: ( i in I & G = F . i & f = 1_ (product F) implies f . i = 1_ G )
assume A1: ( i in I & G = F . i & f = 1_ (product F) ) ; :: thesis: f . i = 1_ G
set GP = product F;
f in the carrier of (product F) by A1;
then A2: f in product (Carrier F) by Def2;
then reconsider e = f . i as Element of G by A1, Lm1;

now

let h be Element of G; :: thesis: ( h * e = h & e * h = h )
A3: dom (Carrier F) = I by PARTFUN1:def 4;
defpred S₁[ set , set ] means ( ( $1 = i implies $2 = h ) & ( $1 <> i implies ex H being non empty Group-like multMagma st
( H = F . $1 & $2 = 1_ H ) ) );
A4: for j being set st j in I holds
ex k being set st S₁[j,k]

proof

let j be set ; :: thesis: ( j in I implies ex k being set st S₁[j,k] )
assume A5: j in I ; :: thesis: ex k being set st S₁[j,k]

per cases ( j = i or j <> i ) ;

suppose j = i ; :: thesis: ex k being set st S₁[j,k]

hence ex k being set st S₁[j,k] ; :: thesis: verum

end;

suppose A6: j <> i ; :: thesis: ex k being set st S₁[j,k]

consider Fj being non empty Group-like multMagma such that
A7: Fj = F . j by A5, Def3;
take 1_ Fj ; :: thesis: S₁[j, 1_ Fj]
thus ( j = i implies 1_ Fj = h ) by A6; :: 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 A7; :: thesis: verum

end;

end;

end;

consider g being ManySortedSet of such that
A8: for j being set st j in I holds
S₁[j,g . j] from PBOOLE:sch 3(A4);
A9: dom g = I by PARTFUN1:def 4;

now

let j be set ; :: thesis: ( j in dom g implies g . b₁ in (Carrier F) . b₁ )
assume A10: j in dom g ; :: thesis: g . b₁ in (Carrier F) . b₁
then consider R being 1-sorted such that
A11: ( R = F . j & (Carrier F) . j = the carrier of R ) by A9, PRALG_1:def 13;

per cases ( i = j or j <> i ) ;

suppose A12: i = j ; :: thesis: g . b₁ in (Carrier F) . b₁

then g . j = h by A8, A9, A10;
hence g . j in (Carrier F) . j by A1, A11, A12; :: thesis: verum

end;

suppose j <> i ; :: thesis: g . b₁ in (Carrier F) . b₁

then consider H being non empty Group-like multMagma such that
A13: ( H = F . j & g . j = 1_ H ) by A8, A9, A10;
thus g . j in (Carrier F) . j by A11, A13; :: thesis: verum

end;

end;

end;

then A14: g in product (Carrier F) by A3, A9, CARD_3:18;
then reconsider g1 = g as Element of (product F) by Def2;
consider Fi being non empty multMagma , m being Function such that
A15: ( Fi = F . i & m = the multF of (product F) . g,f & m . i = the multF of Fi . (g . i),(f . i) ) by A1, A2, A14, Def2;
A16: g1 * (1_ (product F)) = g1 by GROUP_1:def 5;
g . i = h by A1, A8;
hence h * e = h by A1, A15, A16; :: thesis: e * h = h
consider Fi being non empty multMagma , m being Function such that
A17: ( Fi = F . i & m = the multF of (product F) . f,g & m . i = the multF of Fi . (f . i),(g . i) ) by A1, A2, A14, Def2;
A18: (1_ (product F)) * g1 = g1 by GROUP_1:def 5;
g . i = h by A1, A8;
hence e * h = h by A1, A17, A18; :: thesis: verum

end;

hence f . i = 1_ G by GROUP_1:10; :: thesis: verum