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₁ 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₁[ 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₁[j,k]

proof

let j be object ; :: thesis: ( j in I implies ex k being object st S₁[j,k] )
assume A5: 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 A6: j <> i ; :: thesis: ex k being object st S₁[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₁[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
S₁[j,g . j] from PBOOLE:sch 3(A4);
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

let j be object ; :: thesis: ( j in dom g implies g . b₁ in (Carrier F) . b₁ )
assume A10: j in dom g ; :: thesis: g . b₁ in (Carrier F) . b₁
then A11: 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 A12: i = j ; :: thesis: g . b₁ in (Carrier F) . b₁

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

end;

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

then ex H being non empty multMagma ex a being Element of H st
( H = F . j & g . j = a ) by A7, A10;
hence g . j in (Carrier F) . j by A11; :: thesis: verum

end;

end;

end;

dom (Carrier F) = 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₁ being Element of the carrier of G st
( h * b₁ = ei & b₁ * 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