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 () 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 () 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 () 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 () 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 () 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 (); :: 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 () = I by PARTFUN1:def 2;
A3: the carrier of () = product () 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 ;
A9: F . q = (q .--> K) . q by
.= K by ;
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 ;
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 ;
i <> q by A1;
then A15: not i in dom (q .--> K) by FUNCOP_1:75;
A16: i in I by ;
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 & () . i = the carrier of R ) by ;
then A18: (Carrier F0) . i = () . i by ;
ex g being Function st
( y = g & dom g = dom () & ( for i being object st i in dom () holds
g . i in () . i ) ) by ;
then y . i in () . i by ;
hence ( y0 . i in (Carrier F0) . i & y0 . i in F0 . i ) by ; :: 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 ;
A20: dom y = I by PARTFUN1:def 2;
then y | {q} = q .--> k by FUNCT_7:6;
then y = (y | I0) +* (q .--> k) by ;
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 ; :: thesis: verum