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