let i, I be set ; 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; 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; 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 ; 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); 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; ( 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
; 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; verum