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 () such that A3: for h being Element of () holds
( h * e = h & e * h = h & ex g being Element of () 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 () by Def2;
reconsider ei = f . i as Element of G by A1, A2, Lm1;
take ei ; :: according to GROUP_1:def 2 :: thesis: for b1 being Element of the carrier of G holds
( b1 * ei = b1 & ei * b1 = b1 & ex b2 being Element of the carrier of G st
( b1 * b2 = ei & b2 * b1 = ei ) )

let h be Element of G; :: thesis: ( h * ei = h & ei * h = h & ex b1 being Element of the carrier of G st
( h * b1 = ei & b1 * h = ei ) )

defpred S1[ 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 S1[j,k]
proof
let j be object ; :: thesis: ( j in I implies ex k being object st S1[j,k] )
assume A5: 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 A6: j <> i ; :: thesis: ex k being object st S1[j,k]
j in dom F by ;
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: S1[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;
end;
end;
consider g being ManySortedSet of I such that
A7: for j being object st j in I holds
S1[j,g . j] from A8: dom g = I by PARTFUN1:def 2;
A9: 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 A10: j in dom g ; :: thesis: g . b1 in () . b1
then A11: ex R being 1-sorted st
( R = F . j & () . j = the carrier of R ) by PRALG_1:def 15;
per cases ( i = j or j <> i ) ;
suppose A12: i = j ; :: thesis: g . b1 in () . b1
then g . j = h by ;
hence g . j in () . j by A2, A11, A12; :: thesis: verum
end;
suppose j <> i ; :: thesis: g . b1 in () . b1
then ex H being non empty multMagma ex a being Element of H st
( H = F . j & g . j = a ) by ;
hence g . j in () . j by A11; :: thesis: verum
end;
end;
end;
dom () = I by PARTFUN1:def 2;
then reconsider g = g as Element of product () by ;
A13: g . i = h by A1, A7;
reconsider g1 = g as Element of () 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 b1 being Element of the carrier of G st
( h * b1 = ei & b1 * h = ei )

consider gg being Element of () such that
A15: g1 * gg = e and
A16: gg * g1 = e by A3;
reconsider r = gg as Element of product () 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