let q be set ; :: thesis: for F being multMagma-Family of {q}

for G being non empty multMagma st F = q .--> G holds

for y being {q} -defined the carrier of b_{2} -valued total Function holds

( y in the carrier of (product F) & y . q in the carrier of G & y = q .--> (y . q) )

let F be multMagma-Family of {q}; :: thesis: for G being non empty multMagma st F = q .--> G holds

for y being {q} -defined the carrier of b_{1} -valued total Function holds

( y in the carrier of (product F) & y . q in the carrier of G & y = q .--> (y . q) )

let G be non empty multMagma ; :: thesis: ( F = q .--> G implies for y being {q} -defined the carrier of G -valued total Function holds

( y in the carrier of (product F) & y . q in the carrier of G & y = q .--> (y . q) ) )

assume A1: F = q .--> G ; :: thesis: for y being {q} -defined the carrier of G -valued total Function holds

( y in the carrier of (product F) & y . q in the carrier of G & y = q .--> (y . q) )

A2: q in {q} by TARSKI:def 1;

A3: the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;

ex R being 1-sorted st

( R = F . q & (Carrier F) . q = the carrier of R ) by PRALG_1:def 15, A2;

then A4: (Carrier F) . q = the carrier of G by A2, A1, FUNCOP_1:7;

A5: dom (Carrier F) = {q} by PARTFUN1:def 2;

let y be {q} -defined the carrier of G -valued total Function; :: thesis: ( y in the carrier of (product F) & y . q in the carrier of G & y = q .--> (y . q) )

A6: dom y = {q} by PARTFUN1:def 2;

then y . q in rng y by FUNCT_1:3, A2;

then reconsider z = y . q as Element of G ;

A7: for x being object st x in dom y holds

y . x = z by TARSKI:def 1;

for G being non empty multMagma st F = q .--> G holds

for y being {q} -defined the carrier of b

( y in the carrier of (product F) & y . q in the carrier of G & y = q .--> (y . q) )

let F be multMagma-Family of {q}; :: thesis: for G being non empty multMagma st F = q .--> G holds

for y being {q} -defined the carrier of b

( y in the carrier of (product F) & y . q in the carrier of G & y = q .--> (y . q) )

let G be non empty multMagma ; :: thesis: ( F = q .--> G implies for y being {q} -defined the carrier of G -valued total Function holds

( y in the carrier of (product F) & y . q in the carrier of G & y = q .--> (y . q) ) )

assume A1: F = q .--> G ; :: thesis: for y being {q} -defined the carrier of G -valued total Function holds

( y in the carrier of (product F) & y . q in the carrier of G & y = q .--> (y . q) )

A2: q in {q} by TARSKI:def 1;

A3: the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;

ex R being 1-sorted st

( R = F . q & (Carrier F) . q = the carrier of R ) by PRALG_1:def 15, A2;

then A4: (Carrier F) . q = the carrier of G by A2, A1, FUNCOP_1:7;

A5: dom (Carrier F) = {q} by PARTFUN1:def 2;

let y be {q} -defined the carrier of G -valued total Function; :: thesis: ( y in the carrier of (product F) & y . q in the carrier of G & y = q .--> (y . q) )

A6: dom y = {q} by PARTFUN1:def 2;

then y . q in rng y by FUNCT_1:3, A2;

then reconsider z = y . q as Element of G ;

A7: for x being object st x in dom y holds

y . x = z by TARSKI:def 1;

now :: thesis: for i being object st i in dom y holds

y . i in (Carrier F) . i

hence
( y in the carrier of (product F) & y . q in the carrier of G & y = q .--> (y . q) )
by A7, FUNCOP_1:11, A5, A6, CARD_3:9, A3; :: thesis: verumy . i in (Carrier F) . i

let i be object ; :: thesis: ( i in dom y implies y . i in (Carrier F) . i )

assume A8: i in dom y ; :: thesis: y . i in (Carrier F) . i

then A9: i = q by TARSKI:def 1;

y . i = z by TARSKI:def 1, A8;

hence y . i in (Carrier F) . i by A4, A9; :: thesis: verum

end;assume A8: i in dom y ; :: thesis: y . i in (Carrier F) . i

then A9: i = q by TARSKI:def 1;

y . i = z by TARSKI:def 1, A8;

hence y . i in (Carrier F) . i by A4, A9; :: thesis: verum