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

for x being I -defined total Function st ( for p being Element of I holds x . p in F . p ) holds

x in the carrier of (product F)

let F be Group-like associative multMagma-Family of I; :: thesis: for x being I -defined total Function st ( for p being Element of I holds x . p in F . p ) holds

x in the carrier of (product F)

let x be I -defined total Function; :: thesis: ( ( for p being Element of I holds x . p in F . p ) implies x in the carrier of (product F) )

assume A1: for p being Element of I holds x . p in F . p ; :: thesis: x in the carrier of (product F)

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 x = I by PARTFUN1:def 2;

for x being I -defined total Function st ( for p being Element of I holds x . p in F . p ) holds

x in the carrier of (product F)

let F be Group-like associative multMagma-Family of I; :: thesis: for x being I -defined total Function st ( for p being Element of I holds x . p in F . p ) holds

x in the carrier of (product F)

let x be I -defined total Function; :: thesis: ( ( for p being Element of I holds x . p in F . p ) implies x in the carrier of (product F) )

assume A1: for p being Element of I holds x . p in F . p ; :: thesis: x in the carrier of (product F)

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 x = I by PARTFUN1:def 2;

now :: thesis: for i being object st i in dom (Carrier F) holds

x . i in (Carrier F) . i

hence
x in the carrier of (product F)
by A3, A2, A4, CARD_3:def 5; :: thesis: verumx . i in (Carrier F) . i

let i be object ; :: thesis: ( i in dom (Carrier F) implies x . i in (Carrier F) . i )

assume A5: i in dom (Carrier F) ; :: thesis: x . i in (Carrier F) . i

consider R being 1-sorted such that

A6: ( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def 15, A5;

reconsider i0 = i as Element of I by A5;

x . i0 in the carrier of R by A6, STRUCT_0:def 5, A1;

hence x . i in (Carrier F) . i by A6; :: thesis: verum

end;assume A5: i in dom (Carrier F) ; :: thesis: x . i in (Carrier F) . i

consider R being 1-sorted such that

A6: ( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def 15, A5;

reconsider i0 = i as Element of I by A5;

x . i0 in the carrier of R by A6, STRUCT_0:def 5, A1;

hence x . i in (Carrier F) . i by A6; :: thesis: verum