let I0, I be non empty finite set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: ( 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) ) ; :: thesis: 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; :: thesis: ( 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; :: thesis: 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; :: thesis: verum