let I, i be set ; :: thesis: for f, g, h being Function
for F being multMagma-Family of
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
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 ; :: 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 & g = q ) and
A4: ( h = p * q & f . i = x & g . i = y ) ; :: thesis: x * y = h . i
set GP = product F;
( p in the carrier of (product F) & q in the carrier of (product F) ) ;
then ( f in product (Carrier F) & g in product (Carrier F) ) by A3, Def2;
then consider Fi being non empty multMagma , m being Function such that
A5: ( Fi = F . i & m = the multF of (product F) . f,g & m . i = the multF of Fi . (f . i),(g . i) ) by A1, Def2;
thus x * y = h . i by A2, A3, A4, A5; :: thesis: verum