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_{1}[ 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_{1}[x,y]

A3: for x being Element of the carrier of (F . i) holds S_{1}[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)

take f ; :: thesis: ( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) )

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

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

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

A2: for x being Element of (F . i) ex y being Element of (ProjGroup (F,i)) st S

proof

consider f being Function of (F . i), the carrier of (ProjGroup (F,i)) such that
let x be Element of (F . i); :: thesis: ex y being Element of (ProjGroup (F,i)) st S_{1}[x,y]

(1_ (product F)) +* (i,x) in ProjSet (F,i) by Def1;

hence ex y being Element of (ProjGroup (F,i)) st S_{1}[x,y]
by A1; :: thesis: verum

end;(1_ (product F)) +* (i,x) in ProjSet (F,i) by Def1;

hence ex y being Element of (ProjGroup (F,i)) st S

A3: for x being Element of the carrier of (F . i) holds S

for a, b being Element of (F . i) holds f . (a * b) = (f . a) * (f . b)

proof

then reconsider f = f as Homomorphism of (F . i),(ProjGroup (F,i)) by GROUP_6:def 6;
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;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

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

then A8:
the carrier of (ProjGroup (F,i)) c= rng f
by TARSKI:def 3;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;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

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

then
f is one-to-one
by FUNCT_2:19;
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;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

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