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_ (product F) 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_ (product F) 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_ (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 that
A1: i in I and
A2: G = F . i and
A3: f = 1_ (product F) ; :: thesis: f . i = 1_ G
set GP = product F;
f in the carrier of (product F) by A3;
then A4: f in product (Carrier F) 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 S₁[ 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 S₁[j,k]

proof

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

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

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

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

end;

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

consider Fj being non empty Group-like multMagma such that
A8: Fj = F . j by A6, Def3;
take 1_ Fj ; :: thesis: S₁[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
S₁[j,g . j] from PBOOLE:sch 3(A5);
A10: dom g = I by PARTFUN1:def 2;

A11: now :: thesis: for j being object st j in dom g holds
g . j in (Carrier F) . j

let j be object ; :: thesis: ( j in dom g implies g . b₁ in (Carrier F) . b₁ )
assume A12: j in dom g ; :: thesis: g . b₁ in (Carrier F) . b₁
then A13: ex R being 1-sorted st
( R = F . j & (Carrier F) . j = the carrier of R ) by PRALG_1:def 15;

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

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

then g . j = h by A9, A12;
hence g . j in (Carrier F) . j by A2, A13, A14; :: thesis: verum

end;

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

then ex H being non empty Group-like multMagma st
( H = F . j & g . j = 1_ H ) by A9, A12;
hence g . j in (Carrier F) . j by A13; :: thesis: verum

end;

end;

end;

dom (Carrier F) = I by PARTFUN1:def 2;
then A15: g in product (Carrier F) by A10, A11, CARD_3:9;
then reconsider g1 = g as Element of (product F) by Def2;
A16: g1 * (1_ (product F)) = 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 (product F) . (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_ (product F)) * 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 (product F) . (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