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

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

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

then
g +* (q .--> k) in product (Carrier F)
by A8, CARD_3:def 5;
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

end;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;

end;

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;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

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;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

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