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) ) )
A1: the carrier of (ProjGroup (F,i)) = ProjSet (F,i) by Def2;
defpred S₁[ set , set ] means $2 = (1_ (product F)) +* (i,$1);
A2: 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 Def1;
hence ex y being Element of (ProjGroup (F,i)) st S₁[x,y] by A1; :: thesis: verum

end;

consider f being Function of (F . i), the carrier of (ProjGroup (F,i)) such that
A3: for x being Element of the carrier of (F . i) holds S₁[x,f . x] from FUNCT_2:sch 3(A2);
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)
A4: f . a = (1_ (product F)) +* (i,a) by A3;
A5: f . b = (1_ (product F)) +* (i,b) by A3;
A6: f . (a * b) = (1_ (product F)) +* (i,(a * b)) by A3;
the carrier of (ProjGroup (F,i)) = ProjSet (F,i) by Def2;
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:43
.= f . (a * b) by A6, A4, A5, Th3 ; :: thesis: verum

end;

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

now :: thesis: for x being object st x in the carrier of (ProjGroup (F,i)) holds
x in rng f

let x be object ; :: 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
A7: x = (1_ (product F)) +* (i,g) by Def1, A1;
x = f . g by A7, A3;
hence x in rng f by FUNCT_2:4; :: thesis: verum

end;

then A8: the carrier of (ProjGroup (F,i)) c= rng f by TARSKI:def 3;
rng f = the carrier of (ProjGroup (F,i)) by A8, XBOOLE_0:def 10;
then A9: f is onto by FUNCT_2:def 3;
for x1, x2 being object 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 object ; :: thesis: ( x1 in the carrier of (F . i) & x2 in the carrier of (F . i) & f . x1 = f . x2 implies x1 = x2 )
assume A10: ( 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) ;
A11: f . xx1 = (1_ (product F)) +* (i,xx1) by A3;
A12: (1_ (product F)) +* (i,xx1) = (1_ (product F)) +* (i,xx2) by A10, A11, A3;
the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;
then A13: dom (1_ (product F)) = I by PARTFUN1:def 2;
thus x1 = ((1_ (product F)) +* (i .--> xx1)) . i by FUNCT_7:94
.= ((1_ (product F)) +* (i,xx1)) . i by A13, FUNCT_7:def 3
.= ((1_ (product F)) +* (i .--> xx2)) . i by A13, A12, FUNCT_7:def 3
.= x2 by FUNCT_7:94 ; :: thesis: verum

end;

then f is one-to-one by FUNCT_2:19;
hence f is bijective by A9; :: 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 A3; :: thesis: verum