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 H, K being Group
for q being Element of I
for k being Element of K
for g being Function st g in the carrier of (product F0) & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
g +* (q .--> k) in the carrier of (product F)
let F0 be Group-like associative multMagma-Family of I0; :: thesis: for F being Group-like associative multMagma-Family of I
for H, K being Group
for q being Element of I
for k being Element of K
for g being Function st g in the carrier of (product F0) & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
g +* (q .--> k) in the carrier of (product F)
let F be Group-like associative multMagma-Family of I; :: thesis: for H, K being Group
for q being Element of I
for k being Element of K
for g being Function st g in the carrier of (product F0) & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
g +* (q .--> k) in the carrier of (product F)
let H, K be Group; :: thesis: for q being Element of I
for k being Element of K
for g being Function st g in the carrier of (product F0) & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
g +* (q .--> k) in the carrier of (product F)
let q be Element of I; :: thesis: for k being Element of K
for g being Function st g in the carrier of (product F0) & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
g +* (q .--> k) in the carrier of (product F)
let k be Element of K; :: thesis: for g being Function st g in the carrier of (product F0) & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
g +* (q .--> k) in the carrier of (product F)
let g be Function; :: thesis: ( g in the carrier of (product F0) & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) implies g +* (q .--> k) in the carrier of (product F) )
assume A1: ( g in the carrier of (product F0) & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) ) ; :: thesis: g +* (q .--> k) in the carrier of (product F)
set HK = <*H,K*>;
A2: dom (Carrier F0) = I0 by PARTFUN1:def 2;
A3: dom (q .--> k) = {q} ;
A4: dom (q .--> K) = {q} ;
A5: dom F0 = I0 by PARTFUN1:def 2;
set w = g +* (q .--> k);
A6: g in product (Carrier F0) by A1, GROUP_7:def 2;
then A7: ex g0 being Function st
( g = g0 & dom g0 = dom (Carrier F0) & ( for y being object st y in dom (Carrier F0) holds
g0 . y in (Carrier F0) . y ) ) by CARD_3:def 5;
dom (g +* (q .--> k)) = (dom g) \/ (dom (q .--> k)) by FUNCT_4:def 1
.= I0 \/ (dom (q .--> k)) by PARTFUN1:def 2, A6
.= I by A1 ;
then A8: dom (g +* (q .--> k)) = dom (Carrier F) by PARTFUN1:def 2;
for x being object st x in dom (Carrier F) holds
(g +* (q .--> k)) . x in (Carrier F) . x

proof

let x be object ; :: thesis: ( x in dom (Carrier F) implies (g +* (q .--> k)) . x in (Carrier F) . x )
assume A9: x in dom (Carrier F) ; :: thesis: (g +* (q .--> k)) . x in (Carrier F) . x

per cases ( x in I0 or x in {q} ) by A1, XBOOLE_0:def 3, A9;

suppose A10: x in I0 ; :: thesis: (g +* (q .--> k)) . x in (Carrier F) . x

A11: not x in {q} by A1, A10, TARSKI:def 1;
then A12: F . x = F0 . x by A1, FUNCT_4:def 1, A5, A4, A9;
consider R1 being 1-sorted such that
A13: ( R1 = F0 . x & (Carrier F0) . x = the carrier of R1 ) by PRALG_1:def 15, A10;
consider R2 being 1-sorted such that
A14: ( R2 = F . x & (Carrier F) . x = the carrier of R2 ) by PRALG_1:def 15, A9;
(g +* (q .--> k)) . x = g . x by FUNCT_4:def 1, A7, A2, A3, A9, A1, A11;
hence (g +* (q .--> k)) . x in (Carrier F) . x by A13, A14, A12, A10, A2, A7; :: thesis: verum

end;

suppose A15: x in {q} ; :: thesis: (g +* (q .--> k)) . x in (Carrier F) . x

then F . x = (q .--> K) . x by A1, FUNCT_4:def 1, A5, A4;
then A16: F . x = K by A15, FUNCOP_1:7;
A17: (g +* (q .--> k)) . x = (q .--> k) . x by A7, A2, A3, A1, FUNCT_4:def 1, A15
.= k by A15, FUNCOP_1:7 ;
ex R2 being 1-sorted st
( R2 = F . x & (Carrier F) . x = the carrier of R2 ) by PRALG_1:def 15, A15;
hence (g +* (q .--> k)) . x in (Carrier F) . x by A17, A16; :: thesis: verum

end;

end;

end;

then g +* (q .--> k) in product (Carrier F) by A8, CARD_3:def 5;
hence g +* (q .--> k) in the carrier of (product F) by GROUP_7:def 2; :: thesis: verum