let i, I be set ; :: thesis: for F being multMagma-Family of I

for G being non empty multMagma st i in I & G = F . i & product F is Group-like holds

G is Group-like

let F be multMagma-Family of I; :: thesis: for G being non empty multMagma st i in I & G = F . i & product F is Group-like holds

G is Group-like

let G be non empty multMagma ; :: thesis: ( i in I & G = F . i & product F is Group-like implies G is Group-like )

assume that

A1: i in I and

A2: G = F . i ; :: thesis: ( not product F is Group-like or G is Group-like )

set GP = product F;

given e being Element of (product F) such that A3: for h being Element of (product F) holds

( h * e = h & e * h = h & ex g being Element of (product F) st

( h * g = e & g * h = e ) ) ; :: according to GROUP_1:def 2 :: thesis: G is Group-like

reconsider f = e as Element of product (Carrier F) by Def2;

reconsider ei = f . i as Element of G by A1, A2, Lm1;

take ei ; :: according to GROUP_1:def 2 :: thesis: for b_{1} being Element of the carrier of G holds

( b_{1} * ei = b_{1} & ei * b_{1} = b_{1} & ex b_{2} being Element of the carrier of G st

( b_{1} * b_{2} = ei & b_{2} * b_{1} = ei ) )

let h be Element of G; :: thesis: ( h * ei = h & ei * h = h & ex b_{1} being Element of the carrier of G st

( h * b_{1} = ei & b_{1} * h = ei ) )

defpred S_{1}[ object , object ] means ( ( $1 = i implies $2 = h ) & ( $1 <> i implies ex H being non empty multMagma ex a being Element of H st

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

A4: for j being object st j in I holds

ex k being object st S_{1}[j,k]

A7: for j being object st j in I holds

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

A8: dom g = I by PARTFUN1:def 2;

then reconsider g = g as Element of product (Carrier F) by A8, A9, CARD_3:9;

A13: g . i = h by A1, A7;

reconsider g1 = g as Element of (product F) by Def2;

A14: e * g1 = g1 by A3;

g1 * e = g1 by A3;

hence ( h * ei = h & ei * h = h ) by A1, A2, A13, A14, Th1; :: thesis: ex b_{1} being Element of the carrier of G st

( h * b_{1} = ei & b_{1} * h = ei )

consider gg being Element of (product F) such that

A15: g1 * gg = e and

A16: gg * g1 = e by A3;

reconsider r = gg as Element of product (Carrier F) by Def2;

reconsider r1 = r . i as Element of G by A1, A2, Lm1;

take r1 ; :: thesis: ( h * r1 = ei & r1 * h = ei )

thus ( h * r1 = ei & r1 * h = ei ) by A1, A2, A13, A15, A16, Th1; :: thesis: verum

for G being non empty multMagma st i in I & G = F . i & product F is Group-like holds

G is Group-like

let F be multMagma-Family of I; :: thesis: for G being non empty multMagma st i in I & G = F . i & product F is Group-like holds

G is Group-like

let G be non empty multMagma ; :: thesis: ( i in I & G = F . i & product F is Group-like implies G is Group-like )

assume that

A1: i in I and

A2: G = F . i ; :: thesis: ( not product F is Group-like or G is Group-like )

set GP = product F;

given e being Element of (product F) such that A3: for h being Element of (product F) holds

( h * e = h & e * h = h & ex g being Element of (product F) st

( h * g = e & g * h = e ) ) ; :: according to GROUP_1:def 2 :: thesis: G is Group-like

reconsider f = e as Element of product (Carrier F) by Def2;

reconsider ei = f . i as Element of G by A1, A2, Lm1;

take ei ; :: according to GROUP_1:def 2 :: thesis: for b

( b

( b

let h be Element of G; :: thesis: ( h * ei = h & ei * h = h & ex b

( h * b

defpred S

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

A4: 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 A5: j in I ; :: thesis: ex k being object st S_{1}[j,k]

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

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

end;

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

j in dom F
by A5, PARTFUN1:def 2;

then F . j in rng F by FUNCT_1:def 3;

then reconsider Fj = F . j as non empty multMagma by Def1;

set a = the Element of Fj;

take the Element of Fj ; :: thesis: S_{1}[j, the Element of Fj]

thus ( j = i implies the Element of Fj = h ) by A6; :: thesis: ( j <> i implies ex H being non empty multMagma ex a being Element of H st

( H = F . j & the Element of Fj = a ) )

thus ( j <> i implies ex H being non empty multMagma ex a being Element of H st

( H = F . j & the Element of Fj = a ) ) ; :: thesis: verum

end;then F . j in rng F by FUNCT_1:def 3;

then reconsider Fj = F . j as non empty multMagma by Def1;

set a = the Element of Fj;

take the Element of Fj ; :: thesis: S

thus ( j = i implies the Element of Fj = h ) by A6; :: thesis: ( j <> i implies ex H being non empty multMagma ex a being Element of H st

( H = F . j & the Element of Fj = a ) )

thus ( j <> i implies ex H being non empty multMagma ex a being Element of H st

( H = F . j & the Element of Fj = a ) ) ; :: thesis: verum

A7: for j being object st j in I holds

S

A8: dom g = I by PARTFUN1:def 2;

A9: 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 A10: j in dom g ; :: thesis: g . b_{1} in (Carrier F) . b_{1}

then A11: ex R being 1-sorted st

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

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

then A11: ex R being 1-sorted st

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

then reconsider g = g as Element of product (Carrier F) by A8, A9, CARD_3:9;

A13: g . i = h by A1, A7;

reconsider g1 = g as Element of (product F) by Def2;

A14: e * g1 = g1 by A3;

g1 * e = g1 by A3;

hence ( h * ei = h & ei * h = h ) by A1, A2, A13, A14, Th1; :: thesis: ex b

( h * b

consider gg being Element of (product F) such that

A15: g1 * gg = e and

A16: gg * g1 = e by A3;

reconsider r = gg as Element of product (Carrier F) by Def2;

reconsider r1 = r . i as Element of G by A1, A2, Lm1;

take r1 ; :: thesis: ( h * r1 = ei & r1 * h = ei )

thus ( h * r1 = ei & r1 * h = ei ) by A1, A2, A13, A15, A16, Th1; :: thesis: verum