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 )

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

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

for i being object st i in dom (Carrier F0) holds
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;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

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