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,(product F) 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,(product F) 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,(product F) 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,(product F); :: 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 F) = product (Carrier F) by GROUP_7:def 2;

ex R being 1-sorted st

( R = F . q & (Carrier F) . q = the carrier of R ) by PRALG_1:def 15, A3;

then A5: (Carrier F) . q = the carrier of G by A1, FUNCOP_1:7, A3;

A6: dom (Carrier F) = {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

for y being object st y in the carrier of (product F) holds

ex x being object st

( x in the carrier of G & y = f . x )

then f is onto by FUNCT_2:def 3;

hence f is bijective by A9; :: thesis: verum

for F being Group-like associative multMagma-Family of {q}

for f being Function of G,(product F) 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,(product F) 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,(product F) 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,(product F); :: 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 F) = product (Carrier F) by GROUP_7:def 2;

ex R being 1-sorted st

( R = F . q & (Carrier F) . q = the carrier of R ) by PRALG_1:def 15, A3;

then A5: (Carrier F) . q = the carrier of G by A1, FUNCOP_1:7, A3;

A6: dom (Carrier F) = {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

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

.= (q .--> x2) . q by A8, A2, A7

.= z2 by FUNCOP_1:7, A3 ; :: thesis: verum

end;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 FUNCOP_1:7, A3

.= (q .--> x2) . q by A8, A2, A7

.= z2 by FUNCOP_1:7, A3 ; :: thesis: verum

for y being object st y in the carrier of (product F) holds

ex x being object st

( x in the carrier of G & y = f . x )

proof

then
rng f = the carrier of (product F)
by FUNCT_2:10;
let y be object ; :: thesis: ( y in the carrier of (product F) implies ex x being object st

( x in the carrier of G & y = f . x ) )

assume y in the carrier of (product F) ; :: 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 (Carrier F) & ( for z being object st z in dom (Carrier F) holds

g . z in (Carrier F) . z ) ) by CARD_3:def 5, A4;

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 TARSKI:def 1, A10;

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 A11, FUNCOP_1:11, A10

.= q .--> x by A10, PARTFUN1:def 2

.= f . x by A2 ; :: thesis: verum

end;( x in the carrier of G & y = f . x ) )

assume y in the carrier of (product F) ; :: 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 (Carrier F) & ( for z being object st z in dom (Carrier F) holds

g . z in (Carrier F) . z ) ) by CARD_3:def 5, A4;

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 TARSKI:def 1, A10;

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 A11, FUNCOP_1:11, A10

.= q .--> x by A10, PARTFUN1:def 2

.= f . x by A2 ; :: thesis: verum

then f is onto by FUNCT_2:def 3;

hence f is bijective by A9; :: thesis: verum