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 (product F)

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 (product F)

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 (product F)

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 (product F)

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 (product F); :: 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 (product F) ;

then A8: g in product (Carrier F) by A4, Def2;

p in the carrier of (product F) ;

then f in product (Carrier F) by A3, Def2;

then ex Fi being non empty multMagma ex m being Function st

( Fi = F . i & m = the multF of (product F) . (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

for F being multMagma-Family of I

for G being non empty multMagma

for p, q being Element of (product F)

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 (product F)

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 (product F)

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 (product F)

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 (product F); :: 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 (product F) ;

then A8: g in product (Carrier F) by A4, Def2;

p in the carrier of (product F) ;

then f in product (Carrier F) by A3, Def2;

then ex Fi being non empty multMagma ex m being Function st

( Fi = F . i & m = the multF of (product F) . (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