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 ()

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 ()

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 ()

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 ()

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 ()

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 ()

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 () )
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 ()
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 ;
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
.= I by A1 ;
then A8: dom (g +* (q .--> k)) = dom () by PARTFUN1:def 2;
for x being object st x in dom () holds
(g +* (q .--> k)) . x in () . x
proof
let x be object ; :: thesis: ( x in dom () implies (g +* (q .--> k)) . x in () . x )
assume A9: x in dom () ; :: thesis: (g +* (q .--> k)) . x in () . x
per cases ( x in I0 or x in {q} ) by ;
suppose A10: x in I0 ; :: thesis: (g +* (q .--> k)) . x in () . x
A11: not x in {q} by ;
then A12: F . x = F0 . x by ;
consider R1 being 1-sorted such that
A13: ( R1 = F0 . x & (Carrier F0) . x = the carrier of R1 ) by ;
consider R2 being 1-sorted such that
A14: ( R2 = F . x & () . x = the carrier of R2 ) by ;
(g +* (q .--> k)) . x = g . x by ;
hence (g +* (q .--> k)) . x in () . x by A13, A14, A12, A10, A2, A7; :: thesis: verum
end;
suppose A15: x in {q} ; :: thesis: (g +* (q .--> k)) . x in () . x
then F . x = (q .--> K) . x by ;
then A16: F . x = K by ;
A17: (g +* (q .--> k)) . x = (q .--> k) . x by
.= k by ;
ex R2 being 1-sorted st
( R2 = F . x & () . x = the carrier of R2 ) by ;
hence (g +* (q .--> k)) . x in () . x by ; :: thesis: verum
end;
end;
end;
then g +* (q .--> k) in product () by ;
hence g +* (q .--> k) in the carrier of () by GROUP_7:def 2; :: thesis: verum