let G be Group; :: thesis: for q being set
for F being Group-like associative multMagma-Family of {q}
for f being Function of G,() st F = q .--> G & ( for x being Element of G holds f . x = q .--> x ) holds
f is bijective

let q be set ; :: thesis: for F being Group-like associative multMagma-Family of {q}
for f being Function of G,() st F = q .--> G & ( for x being Element of G holds f . x = q .--> x ) holds
f is bijective

let F be Group-like associative multMagma-Family of {q}; :: thesis: for f being Function of G,() st F = q .--> G & ( for x being Element of G holds f . x = q .--> x ) holds
f is bijective

let f be Function of G,(); :: thesis: ( F = q .--> G & ( for x being Element of G holds f . x = q .--> x ) implies f is bijective )
assume A1: F = q .--> G ; :: thesis: ( ex x being Element of G st not f . x = q .--> x or f is bijective )
assume A2: for x being Element of G holds f . x = q .--> x ; :: thesis: f is bijective
A3: q in {q} by TARSKI:def 1;
A4: the carrier of () = product () by GROUP_7:def 2;
ex R being 1-sorted st
( R = F . q & () . q = the carrier of R ) by ;
then A5: (Carrier F) . q = the carrier of G by ;
A6: dom () = {q} by PARTFUN1:def 2;
for x1, x2 being object st x1 in the carrier of G & x2 in the carrier of G & f . x1 = f . x2 holds
x1 = x2
proof
let z1, z2 be object ; :: thesis: ( z1 in the carrier of G & z2 in the carrier of G & f . z1 = f . z2 implies z1 = z2 )
assume A7: ( z1 in the carrier of G & z2 in the carrier of G & f . z1 = f . z2 ) ; :: thesis: z1 = z2
then reconsider x1 = z1, x2 = z2 as Element of G ;
A8: f . x2 = q .--> x2 by A2;
thus z1 = (q .--> x1) . q by
.= (q .--> x2) . q by A8, A2, A7
.= z2 by ; :: thesis: verum
end;
then A9: f is one-to-one by FUNCT_2:19;
for y being object st y in the carrier of () holds
ex x being object st
( x in the carrier of G & y = f . x )
proof
let y be object ; :: thesis: ( y in the carrier of () implies ex x being object st
( x in the carrier of G & y = f . x ) )

assume y in the carrier of () ; :: thesis: ex x being object st
( x in the carrier of G & y = f . x )

then consider g being Function such that
A10: ( y = g & dom g = dom () & ( for z being object st z in dom () holds
g . z in () . z ) ) by ;
reconsider x = g . q as Element of G by A5, A10, A3, A6;
A11: for z being object st z in dom g holds
g . z = x by ;
take x ; :: thesis: ( x in the carrier of G & y = f . x )
thus x in the carrier of G ; :: thesis: y = f . x
thus y = (dom g) --> x by
.= q .--> x by
.= f . x by A2 ; :: thesis: verum
end;
then rng f = the carrier of () by FUNCT_2:10;
then f is onto by FUNCT_2:def 3;
hence f is bijective by A9; :: thesis: verum