let I, i be set ; :: thesis: for F being multMagma-Family of
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 ; :: 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 A1: ( i in I & 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 A2: 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 3 :: 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, Lm1;
take ei ; :: according to GROUP_1:def 3 :: thesis: for b₁ being Element of the carrier of G holds
( b₁ * ei = b₁ & ei * b₁ = b₁ & ex b₂ being Element of the carrier of G st
( b₁ * b₂ = ei & b₂ * b₁ = ei ) )
let h be Element of G; :: thesis: ( h * ei = h & ei * h = h & ex b₁ being Element of the carrier of G st
( h * b₁ = ei & b₁ * h = ei ) )
defpred S₁[ set , set ] 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 ) ) );
A3: 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 A4: 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 A5: j <> i ; :: thesis: ex k being set st S₁[j,k]

j in dom F by A4, PARTFUN1:def 4;
then F . j in rng F by FUNCT_1:def 5;
then reconsider Fj = F . j as non empty multMagma by Def1;
consider a being Element of Fj;
take a ; :: thesis: S₁[j,a]
thus ( j = i implies a = h ) by A5; :: thesis: ( j <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . j & a = a ) )
thus ( j <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . j & a = a ) ) ; :: thesis: verum

end;

end;

end;

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

now

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

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

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

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

end;

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

then consider H being non empty multMagma , a being Element of H such that
A12: ( H = F . j & g . j = a ) by A6, A7, A9;
thus g . j in (Carrier F) . j by A10, A12; :: thesis: verum

end;

end;

end;

then reconsider g = g as Element of product (Carrier F) by A7, A8, CARD_3:18;
reconsider g1 = g as Element of (product F) by Def2;
A13: g . i = h by A1, A6;
( g1 * e = g1 & e * g1 = g1 ) by A2;
hence ( h * ei = h & ei * h = h ) by A1, A13, Th4; :: thesis: ex b₁ being Element of the carrier of G st
( h * b₁ = ei & b₁ * h = ei )
consider gg being Element of (product F) such that
A14: ( g1 * gg = e & gg * g1 = e ) by A2;
reconsider r = gg as Element of product (Carrier F) by Def2;
reconsider r1 = r . i as Element of G by A1, Lm1;
take r1 ; :: thesis: ( h * r1 = ei & r1 * h = ei )
thus ( h * r1 = ei & r1 * h = ei ) by A1, A13, A14, Th4; :: thesis: verum