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 K being Group
for q being Element of I
for x being Element of (product F) st not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
ex x0 being I0 -defined total Function ex k being Element of K st
( x0 in product F0 & x = x0 +* (q .--> k) & ( for p being Element of I0 holds x0 . p in F0 . p ) )
let F0 be Group-like associative multMagma-Family of I0; for F being Group-like associative multMagma-Family of I
for K being Group
for q being Element of I
for x being Element of (product F) st not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
ex x0 being I0 -defined total Function ex k being Element of K st
( x0 in product F0 & x = x0 +* (q .--> k) & ( for p being Element of I0 holds x0 . p in F0 . p ) )
let F be Group-like associative multMagma-Family of I; for K being Group
for q being Element of I
for x being Element of (product F) st not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
ex x0 being I0 -defined total Function ex k being Element of K st
( x0 in product F0 & x = x0 +* (q .--> k) & ( for p being Element of I0 holds x0 . p in F0 . p ) )
let K be Group; for q being Element of I
for x being Element of (product F) st not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
ex x0 being I0 -defined total Function ex k being Element of K st
( x0 in product F0 & x = x0 +* (q .--> k) & ( for p being Element of I0 holds x0 . p in F0 . p ) )
let q be Element of I; for x being Element of (product F) st not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
ex x0 being I0 -defined total Function ex k being Element of K st
( x0 in product F0 & x = x0 +* (q .--> k) & ( for p being Element of I0 holds x0 . p in F0 . p ) )
let x be Element of (product F); ( not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) implies ex x0 being I0 -defined total Function ex k being Element of K st
( x0 in product F0 & x = x0 +* (q .--> k) & ( for p being Element of I0 holds x0 . p in F0 . p ) ) )
assume A1:
( not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) )
; ex x0 being I0 -defined total Function ex k being Element of K st
( x0 in product F0 & x = x0 +* (q .--> k) & ( for p being Element of I0 holds x0 . p in F0 . p ) )
reconsider y = x as I -defined total Function by Lm6;
A2:
dom (Carrier F) = I
by PARTFUN1:def 2;
A3:
the carrier of (product F) = product (Carrier F)
by GROUP_7:def 2;
A4:
dom F0 = I0
by PARTFUN1:def 2;
A6:
q in {q}
by TARSKI:def 1;
A7:
q in dom (q .--> K)
by TARSKI:def 1;
A8:
q in (dom F0) \/ (dom (q .--> K))
by A6, XBOOLE_0:def 3;
A9: F . q =
(q .--> K) . q
by A7, A8, A1, FUNCT_4:def 1
.=
K
by FUNCOP_1:7, A6
;
ex R being non empty multMagma st
( R = F . q & y . q in the carrier of R )
by Lm7;
then reconsider k = y . q as Element of K by A9;
reconsider y0 = y | I0 as I0 -defined Function ;
A10:
the carrier of (product F0) = product (Carrier F0)
by GROUP_7:def 2;
I = dom y
by PARTFUN1:def 2;
then A11:
dom y0 = I0
by RELAT_1:62, A1, XBOOLE_1:7;
then reconsider y0 = y0 as I0 -defined total Function by PARTFUN1:def 2;
A12:
dom (Carrier F0) = I0
by PARTFUN1:def 2;
A13:
for i being Element of I0 holds
( y0 . i in (Carrier F0) . i & y0 . i in F0 . i )
proof
let i be
Element of
I0;
( y0 . i in (Carrier F0) . i & y0 . i in F0 . i )
A14:
i in (dom F0) \/ (dom (q .--> K))
by A4, XBOOLE_0:def 3;
i <> q
by A1;
then A15:
not
i in dom (q .--> K)
by FUNCOP_1:75;
A16:
i in I
by TARSKI:def 3, XBOOLE_1:7, A1;
consider R being
1-sorted such that A17:
(
R = F0 . i &
(Carrier F0) . i = the
carrier of
R )
by PRALG_1:def 15;
ex
R being
1-sorted st
(
R = F . i &
(Carrier F) . i = the
carrier of
R )
by A16, PRALG_1:def 15;
then A18:
(Carrier F0) . i = (Carrier F) . i
by A15, A14, FUNCT_4:def 1, A1, A17;
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, A3;
then
y . i in (Carrier F) . i
by A16, A2;
hence
(
y0 . i in (Carrier F0) . i &
y0 . i in F0 . i )
by A17, FUNCT_1:49, A18;
verum
end;
for i being object st i in dom (Carrier F0) holds
y0 . i in (Carrier F0) . i
by A13;
then A19:
y0 in the carrier of (product F0)
by A10, A11, A12, CARD_3:def 5;
A20:
dom y = I
by PARTFUN1:def 2;
then
y | {q} = q .--> k
by FUNCT_7:6;
then
y = (y | I0) +* (q .--> k)
by A1, A20, FUNCT_4:70;
hence
ex x0 being I0 -defined total Function ex k being Element of K st
( x0 in product F0 & x = x0 +* (q .--> k) & ( for p being Element of I0 holds x0 . p in F0 . p ) )
by A19, STRUCT_0:def 5, A13; verum