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;

now :: thesis: for i being object st i in dom (Carrier F) holds
x . 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;

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