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_ ()) +* (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_ ()) +* (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_ ()) +* (i,x) ) )

A1: the carrier of (ProjGroup (F,i)) = ProjSet (F,i) by Def2;
defpred S1[ set , set ] means \$2 = (1_ ()) +* (i,\$1);
A2: for x being Element of (F . i) ex y being Element of (ProjGroup (F,i)) st S1[x,y]
proof
let x be Element of (F . i); :: thesis: ex y being Element of (ProjGroup (F,i)) st S1[x,y]
(1_ ()) +* (i,x) in ProjSet (F,i) by Def1;
hence ex y being Element of (ProjGroup (F,i)) st S1[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 S1[x,f . x] from 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_ ()) +* (i,a) by A3;
A5: f . b = (1_ ()) +* (i,b) by A3;
A6: f . (a * b) = (1_ ()) +* (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 () 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_ ()) +* (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_ ()) +* (i,g) by ;
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 ;
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_ ()) +* (i,xx1) by A3;
A12: (1_ ()) +* (i,xx1) = (1_ ()) +* (i,xx2) by A10, A11, A3;
the carrier of () = product () by GROUP_7:def 2;
then A13: dom (1_ ()) = I by PARTFUN1:def 2;
thus x1 = ((1_ ()) +* (i .--> xx1)) . i by FUNCT_7:94
.= ((1_ ()) +* (i,xx1)) . i by
.= ((1_ ()) +* (i .--> xx2)) . i by
.= 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_ ()) +* (i,x)
thus for x being Element of (F . i) holds f . x = (1_ ()) +* (i,x) by A3; :: thesis: verum