let I be non empty set ; :: thesis: for F being multMagma-Family of I
for x being Function
for i being Element of I st x in product F holds
x . i in F . i
let F be multMagma-Family of I; :: thesis: for x being Function
for i being Element of I st x in product F holds
x . i in F . i
let x be Function; :: thesis: for i being Element of I st x in product F holds
x . i in F . i
let i be Element of I; :: thesis: ( x in product F implies x . i in F . i )
assume A1: x in product F ; :: thesis: x . i in F . i
A2: (Carrier F) . i = [#] (F . i) by PENCIL_3:7;
i in I ;
then A4: i in dom (Carrier F) by PARTFUN1:def 2;
x in product (Carrier F) by A1, GROUP_7:def 2;
hence x . i in F . i by A2, A4, CARD_3:9; :: thesis: verum