let I be non empty set ; :: thesis: for F being Group-like associative multMagma-Family of I
for i being Element of I ex f being Homomorphism of (F . i),(ProjGroup (F,i)) st
( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) )
let F be Group-like associative multMagma-Family of I; :: thesis: for i being Element of I ex f being Homomorphism of (F . i),(ProjGroup (F,i)) st
( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) )
let i be Element of I; :: thesis: ex f being Homomorphism of (F . i),(ProjGroup (F,i)) st
( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) )
AS1: the carrier of (ProjGroup (F,i)) = ProjSet (F,i) by defPrjGroup;
defpred S₁[ set , set ] means $2 = (1_ (product F)) +* (i,$1);
P1: for x being Element of (F . i) ex y being Element of (ProjGroup (F,i)) st S₁[x,y]

proof

let x be Element of (F . i); :: thesis: ex y being Element of (ProjGroup (F,i)) st S₁[x,y]
(1_ (product F)) +* (i,x) in ProjSet (F,i) by defPrj;
hence ex y being Element of (ProjGroup (F,i)) st S₁[x,y] by AS1; :: thesis: verum

end;

consider f being Function of (F . i), the carrier of (ProjGroup (F,i)) such that
P2: for x being Element of the carrier of (F . i) holds S₁[x,f . x] from FUNCT_2:sch 3(P1);
for a, b being Element of (F . i) holds f . (a * b) = (f . a) * (f . b)

proof

let a, b be Element of (F . i); :: thesis: f . (a * b) = (f . a) * (f . b)
A3: f . a = (1_ (product F)) +* (i,a) by P2;
A4: f . b = (1_ (product F)) +* (i,b) by P2;
A5: f . (a * b) = (1_ (product F)) +* (i,(a * b)) by P2;
the carrier of (ProjGroup (F,i)) = ProjSet (F,i) by defPrjGroup;
then reconsider ffa = f . a, ffb = f . b as Element of (product F) by TARSKI:def 3;
thus (f . a) * (f . b) = ffa * ffb by GROUP_2:52
.= f . (a * b) by A5, A3, A4, LMPX2 ; :: thesis: verum

end;

then reconsider f = f as Homomorphism of (F . i),(ProjGroup (F,i)) by GROUP_6:def 7;
take f ; :: thesis: ( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) )

now

let x be set ; :: thesis: ( x in the carrier of (ProjGroup (F,i)) implies x in rng f )
assume x in the carrier of (ProjGroup (F,i)) ; :: thesis: x in rng f
then consider g being Element of (F . i) such that
K1: x = (1_ (product F)) +* (i,g) by defPrj, AS1;
x = f . g by K1, P2;
hence x in rng f by FUNCT_2:6; :: thesis: verum

end;

then X1: the carrier of (ProjGroup (F,i)) c= rng f by TARSKI:def 3;
rng f = the carrier of (ProjGroup (F,i)) by X1, XBOOLE_0:def 10;
then P3: f is onto by FUNCT_2:def 3;
for x1, x2 being set st x1 in the carrier of (F . i) & x2 in the carrier of (F . i) & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis: ( x1 in the carrier of (F . i) & x2 in the carrier of (F . i) & f . x1 = f . x2 implies x1 = x2 )
assume ASS: ( x1 in the carrier of (F . i) & x2 in the carrier of (F . i) & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then reconsider xx1 = x1, xx2 = x2 as Element of the carrier of (F . i) ;
A1: f . xx1 = (1_ (product F)) +* (i,xx1) by P2;
A21: (1_ (product F)) +* (i,xx1) = (1_ (product F)) +* (i,xx2) by ASS, A1, P2;
the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;
then ZZZ1: dom (1_ (product F)) = I by PARTFUN1:def 4;
thus x1 = ((1_ (product F)) +* (i .--> xx1)) . i by FUNCT_7:96
.= ((1_ (product F)) +* (i,xx1)) . i by ZZZ1, FUNCT_7:def 3
.= ((1_ (product F)) +* (i .--> xx2)) . i by ZZZ1, FUNCT_7:def 3, A21
.= x2 by FUNCT_7:96 ; :: thesis: verum

end;

then f is one-to-one by FUNCT_2:25;
hence f is bijective by P3; :: thesis: for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x)
thus for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) by P2; :: thesis: verum