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₂ -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₁ -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;

now :: thesis: for i being object st i in dom y holds
y . 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;

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: verum