let I be non empty set ; :: thesis: for F being multMagma-Family of I
for f being Function st f in the carrier of () 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 multMagma-Family of I; :: thesis: for f being Function st f in the carrier of () 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 () 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 () ; :: 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 )

A2: dom () = I by PARTFUN1:def 2;
the carrier of () = product () by GROUP_7:def 2;
then consider g being Function such that
A3: ( f = g & dom g = dom () & ( for y being object st y in dom () holds
g . y in () . y ) ) by ;
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 A4: 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
A5: ( R = F . x & () . x = the carrier of R ) by ;
x in dom F by ;
then R in rng F by ;
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 A4, A3, A2, A5; :: thesis: verum