let I be non empty finite set ; :: thesis: for F being Group-like associative multMagma-Family of I

for f being Function st f in the carrier of (product F) holds

for x being set st x in I holds

ex R being non empty multMagma st

( R = F . x & f . x in the carrier of R )

let F be Group-like associative multMagma-Family of I; :: thesis: for f being Function st f in the carrier of (product F) holds

for x being set st x in I holds

ex R being non empty multMagma st

( R = F . x & f . x in the carrier of R )

let f be Function; :: thesis: ( f in the carrier of (product F) implies for x being set st x in I holds

ex R being non empty multMagma st

( R = F . x & f . x in the carrier of R ) )

assume A1: f in the carrier of (product F) ; :: thesis: for x being set st x in I holds

ex R being non empty multMagma st

( R = F . x & f . x in the carrier of R )

D1: dom (Carrier F) = I by PARTFUN1:def 2;

the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;

then consider g being Function such that

D2: ( f = g & dom g = dom (Carrier F) & ( for y being object st y in dom (Carrier F) holds

g . y in (Carrier F) . y ) ) by CARD_3:def 5, A1;

let x be set ; :: thesis: ( x in I implies ex R being non empty multMagma st

( R = F . x & f . x in the carrier of R ) )

assume A2: x in I ; :: thesis: ex R being non empty multMagma st

( R = F . x & f . x in the carrier of R )

consider R being 1-sorted such that

A4: ( R = F . x & (Carrier F) . x = the carrier of R ) by PRALG_1:def 15, A2;

x in dom F by A2, PARTFUN1:def 2;

then R in rng F by A4, FUNCT_1:3;

then R is non empty multMagma by GROUP_7:def 1;

hence ex R being non empty multMagma st

( R = F . x & f . x in the carrier of R ) by A2, D2, D1, A4; :: thesis: verum

for f being Function st f in the carrier of (product F) holds

for x being set st x in I holds

ex R being non empty multMagma st

( R = F . x & f . x in the carrier of R )

let F be Group-like associative multMagma-Family of I; :: thesis: for f being Function st f in the carrier of (product F) holds

for x being set st x in I holds

ex R being non empty multMagma st

( R = F . x & f . x in the carrier of R )

let f be Function; :: thesis: ( f in the carrier of (product F) implies for x being set st x in I holds

ex R being non empty multMagma st

( R = F . x & f . x in the carrier of R ) )

assume A1: f in the carrier of (product F) ; :: thesis: for x being set st x in I holds

ex R being non empty multMagma st

( R = F . x & f . x in the carrier of R )

D1: dom (Carrier F) = I by PARTFUN1:def 2;

the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;

then consider g being Function such that

D2: ( f = g & dom g = dom (Carrier F) & ( for y being object st y in dom (Carrier F) holds

g . y in (Carrier F) . y ) ) by CARD_3:def 5, A1;

let x be set ; :: thesis: ( x in I implies ex R being non empty multMagma st

( R = F . x & f . x in the carrier of R ) )

assume A2: x in I ; :: thesis: ex R being non empty multMagma st

( R = F . x & f . x in the carrier of R )

consider R being 1-sorted such that

A4: ( R = F . x & (Carrier F) . x = the carrier of R ) by PRALG_1:def 15, A2;

x in dom F by A2, PARTFUN1:def 2;

then R in rng F by A4, FUNCT_1:3;

then R is non empty multMagma by GROUP_7:def 1;

hence ex R being non empty multMagma st

( R = F . x & f . x in the carrier of R ) by A2, D2, D1, A4; :: thesis: verum