let I0, I be non empty finite set ; for F0 being Group-like associative multMagma-Family of I0
for F being Group-like associative multMagma-Family of I
for H, K being Group
for q being Element of I
for G0 being Function of H,(product F0) st G0 is Homomorphism of H,(product F0) & G0 is bijective & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
for G being Function of (product <*H,K*>),(product F) st ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) holds
G is bijective
let F0 be Group-like associative multMagma-Family of I0; for F being Group-like associative multMagma-Family of I
for H, K being Group
for q being Element of I
for G0 being Function of H,(product F0) st G0 is Homomorphism of H,(product F0) & G0 is bijective & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
for G being Function of (product <*H,K*>),(product F) st ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) holds
G is bijective
let F be Group-like associative multMagma-Family of I; for H, K being Group
for q being Element of I
for G0 being Function of H,(product F0) st G0 is Homomorphism of H,(product F0) & G0 is bijective & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
for G being Function of (product <*H,K*>),(product F) st ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) holds
G is bijective
let H, K be Group; for q being Element of I
for G0 being Function of H,(product F0) st G0 is Homomorphism of H,(product F0) & G0 is bijective & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
for G being Function of (product <*H,K*>),(product F) st ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) holds
G is bijective
let q be Element of I; for G0 being Function of H,(product F0) st G0 is Homomorphism of H,(product F0) & G0 is bijective & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
for G being Function of (product <*H,K*>),(product F) st ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) holds
G is bijective
let G0 be Function of H,(product F0); ( G0 is Homomorphism of H,(product F0) & G0 is bijective & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) implies for G being Function of (product <*H,K*>),(product F) st ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) holds
G is bijective )
assume A1:
( G0 is Homomorphism of H,(product F0) & G0 is bijective & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) )
; for G being Function of (product <*H,K*>),(product F) st ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) holds
G is bijective
let G be Function of (product <*H,K*>),(product F); ( ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) implies G is bijective )
assume A2:
for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) )
; G is bijective
set HK = <*H,K*>;
A3:
dom (Carrier F0) = I0
by PARTFUN1:def 2;
A4:
dom (Carrier F) = I
by PARTFUN1:def 2;
A5:
dom F0 = I0
by PARTFUN1:def 2;
A6:
the carrier of (product F) = product (Carrier F)
by GROUP_7:def 2;
for x1, x2 being object st x1 in the carrier of (product <*H,K*>) & x2 in the carrier of (product <*H,K*>) & G . x1 = G . x2 holds
x1 = x2
proof
let z1,
z2 be
object ;
( z1 in the carrier of (product <*H,K*>) & z2 in the carrier of (product <*H,K*>) & G . z1 = G . z2 implies z1 = z2 )
assume A8:
(
z1 in the
carrier of
(product <*H,K*>) &
z2 in the
carrier of
(product <*H,K*>) &
G . z1 = G . z2 )
;
z1 = z2
then reconsider x1 =
z1,
x2 =
z2 as
Element of
(product <*H,K*>) ;
consider h1 being
Element of
H,
k1 being
Element of
K such that A9:
x1 = <*h1,k1*>
by TOPALG_4:1;
consider h2 being
Element of
H,
k2 being
Element of
K such that A10:
x2 = <*h2,k2*>
by TOPALG_4:1;
consider g1 being
Function such that A11:
(
g1 = G0 . h1 &
G . <*h1,k1*> = g1 +* (q .--> k1) )
by A2;
consider g2 being
Function such that A12:
(
g2 = G0 . h2 &
G . <*h2,k2*> = g2 +* (q .--> k2) )
by A2;
reconsider g1 =
g1 as
I0 -defined total Function by Lm6, A11;
reconsider g2 =
g2 as
I0 -defined total Function by Lm6, A12;
reconsider ga =
g1 +* (q .--> k1) as
I -defined total Function by Lm6, A11;
reconsider gb =
g2 +* (q .--> k2) as
I -defined total Function by Lm6, A12;
A15:
for
i being
set st
i in I0 holds
(
ga . i = g1 . i &
gb . i = g2 . i &
F . i = F0 . i )
proof
let i be
set ;
( i in I0 implies ( ga . i = g1 . i & gb . i = g2 . i & F . i = F0 . i ) )
assume A16:
i in I0
;
( ga . i = g1 . i & gb . i = g2 . i & F . i = F0 . i )
A17:
dom g1 = I0
by PARTFUN1:def 2;
A18:
dom g2 = I0
by PARTFUN1:def 2;
A19:
i in (dom g1) \/ (dom (q .--> k1))
by A17, A16, XBOOLE_0:def 3;
A20:
i in (dom g2) \/ (dom (q .--> k2))
by A18, A16, XBOOLE_0:def 3;
A21:
i in (dom F0) \/ (dom (q .--> K))
by A5, A16, XBOOLE_0:def 3;
not
i in dom (q .--> K)
by A1, A16, FUNCOP_1:75;
hence
(
ga . i = g1 . i &
gb . i = g2 . i &
F . i = F0 . i )
by A21, A1, A19, A20, FUNCT_4:def 1;
verum
end;
A24:
dom g2 = I0
by PARTFUN1:def 2;
for
x being
object st
x in dom g1 holds
g1 . x = g2 . x
then A26:
G0 . h1 = G0 . h2
by A11, A12, FUNCT_1:2, PARTFUN1:def 2, A24;
(
ga . q = k1 &
gb . q = k2 )
hence
z1 = z2
by A9, A10, A26, A1, FUNCT_2:19, A11, A12, A8;
verum
end;
then A33:
G is one-to-one
by FUNCT_2:19;
for y being object st y in the carrier of (product F) holds
ex x being object st
( x in the carrier of (product <*H,K*>) & y = G . x )
proof
let y be
object ;
( y in the carrier of (product F) implies ex x being object st
( x in the carrier of (product <*H,K*>) & y = G . x ) )
assume A34:
y in the
carrier of
(product F)
;
ex x being object st
( x in the carrier of (product <*H,K*>) & y = G . x )
then reconsider y =
y as
I -defined total Function by Lm6;
A35:
q in {q}
by TARSKI:def 1;
A36:
q in dom (q .--> K)
by TARSKI:def 1;
A37:
q in (dom F0) \/ (dom (q .--> K))
by A35, XBOOLE_0:def 3;
A38:
F . q =
(q .--> K) . q
by A36, A37, A1, FUNCT_4:def 1
.=
K
by FUNCOP_1:7, A35
;
ex
R being non
empty multMagma st
(
R = F . q &
y . q in the
carrier of
R )
by Lm7, A34;
then reconsider k =
y . q as
Element of
K by A38;
reconsider y0 =
y | I0 as
I0 -defined Function ;
A39:
the
carrier of
(product F0) = product (Carrier F0)
by GROUP_7:def 2;
I = dom y
by PARTFUN1:def 2;
then A40:
dom y0 = I0
by RELAT_1:62, A1, XBOOLE_1:7;
for
i being
object st
i in dom (Carrier F0) holds
y0 . i in (Carrier F0) . i
proof
let i be
object ;
( i in dom (Carrier F0) implies y0 . i in (Carrier F0) . i )
assume A41:
i in dom (Carrier F0)
;
y0 . i in (Carrier F0) . i
then A42:
i in I0
;
A43:
i in (dom F0) \/ (dom (q .--> K))
by A5, A41, XBOOLE_0:def 3;
A44:
not
i in dom (q .--> K)
by A1, A42, FUNCOP_1:75;
A45:
I0 c= I
by XBOOLE_1:7, A1;
A46:
ex
R being
1-sorted st
(
R = F0 . i &
(Carrier F0) . i = the
carrier of
R )
by A41, PRALG_1:def 15;
ex
R being
1-sorted st
(
R = F . i &
(Carrier F) . i = the
carrier of
R )
by A42, A45, PRALG_1:def 15;
then A47:
(Carrier F0) . i = (Carrier F) . i
by A43, FUNCT_4:def 1, A1, A44, A46;
ex
g being
Function st
(
y = g &
dom g = dom (Carrier F) & ( for
i being
object st
i in dom (Carrier F) holds
g . i in (Carrier F) . i ) )
by CARD_3:def 5, A34, A6;
then
y . i in (Carrier F) . i
by A45, A4, A42;
hence
y0 . i in (Carrier F0) . i
by A47, A41, FUNCT_1:49;
verum
end;
then
y0 in the
carrier of
(product F0)
by A40, A3, CARD_3:def 5, A39;
then
y0 in rng G0
by A1, FUNCT_2:def 3;
then consider h being
Element of
H such that A48:
y0 = G0 . h
by FUNCT_2:113;
A49:
dom y = I
by PARTFUN1:def 2;
then
y | {q} = q .--> k
by FUNCT_7:6;
then A50:
y = (y | I0) +* (q .--> k)
by A1, A49, FUNCT_4:70;
consider g being
Function such that A51:
(
g = G0 . h &
G . <*h,k*> = g +* (q .--> k) )
by A2;
thus
ex
x being
object st
(
x in the
carrier of
(product <*H,K*>) &
y = G . x )
by A48, A50, A51;
verum
end;
then
rng G = the carrier of (product F)
by FUNCT_2:10;
then
G is onto
by FUNCT_2:def 3;
hence
G is bijective
by A33; verum