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;

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 )

hence
f . i = 1_ G
by GROUP_1:4; :: thesis: verum( h * e = h & e * h = h )

let h be Element of G; :: thesis: ( h * e = h & e * h = h )

defpred S_{1}[ 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_{1}[j,k]

A9: for j being object st j in I holds

S_{1}[j,g . j]
from PBOOLE:sch 3(A5);

A10: dom g = 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;defpred S

( H = F . $1 & $2 = 1_ H ) ) );

A5: for j being object st j in I holds

ex k being object st S

proof

consider g being ManySortedSet of I such that
let j be object ; :: thesis: ( j in I implies ex k being object st S_{1}[j,k] )

assume A6: j in I ; :: thesis: ex k being object st S_{1}[j,k]

end;assume A6: j in I ; :: thesis: ex k being object st S

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

end;

suppose A7:
j <> i
; :: thesis: ex k being object st S_{1}[j,k]

consider Fj being non empty Group-like multMagma such that

A8: Fj = F . j by A6, Def3;

take 1_ Fj ; :: thesis: S_{1}[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;A8: Fj = F . j by A6, Def3;

take 1_ Fj ; :: thesis: S

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

A9: for j being object st j in I holds

S

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

dom (Carrier F) = I
by PARTFUN1:def 2;g . j in (Carrier F) . j

let j be object ; :: thesis: ( j in dom g implies g . b_{1} in (Carrier F) . b_{1} )

assume A12: j in dom g ; :: thesis: g . b_{1} in (Carrier F) . b_{1}

then A13: ex R being 1-sorted st

( R = F . j & (Carrier F) . j = the carrier of R ) by PRALG_1:def 13;

end;assume A12: j in dom g ; :: thesis: g . b

then A13: ex R being 1-sorted st

( R = F . j & (Carrier F) . j = the carrier of R ) by PRALG_1:def 13;

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