let i, I be set ; :: thesis: for f, g, h being Function
for F being multMagma-Family of I
for G being non empty multMagma
for p, q being Element of ()
for x, y being Element of G st i in I & G = F . i & f = p & g = q & h = p * q & f . i = x & g . i = y holds
x * y = h . i

let f, g, h be Function; :: thesis: for F being multMagma-Family of I
for G being non empty multMagma
for p, q being Element of ()
for x, y being Element of G st i in I & G = F . i & f = p & g = q & h = p * q & f . i = x & g . i = y holds
x * y = h . i

let F be multMagma-Family of I; :: thesis: for G being non empty multMagma
for p, q being Element of ()
for x, y being Element of G st i in I & G = F . i & f = p & g = q & h = p * q & f . i = x & g . i = y holds
x * y = h . i

let G be non empty multMagma ; :: thesis: for p, q being Element of ()
for x, y being Element of G st i in I & G = F . i & f = p & g = q & h = p * q & f . i = x & g . i = y holds
x * y = h . i

let p, q be Element of (); :: thesis: for x, y being Element of G st i in I & G = F . i & f = p & g = q & h = p * q & f . i = x & g . i = y holds
x * y = h . i

let x, y be Element of G; :: thesis: ( i in I & G = F . i & f = p & g = q & h = p * q & f . i = x & g . i = y implies x * y = h . i )
assume that
A1: i in I and
A2: G = F . i and
A3: f = p and
A4: g = q and
A5: h = p * q and
A6: f . i = x and
A7: g . i = y ; :: thesis: x * y = h . i
set GP = product F;
q in the carrier of () ;
then A8: g in product () by ;
p in the carrier of () ;
then f in product () by ;
then ex Fi being non empty multMagma ex m being Function st
( Fi = F . i & m = the multF of () . (f,g) & m . i = the multF of Fi . ((f . i),(g . i)) ) by A1, A8, Def2;
hence x * y = h . i by A2, A3, A4, A5, A6, A7; :: thesis: verum