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 b2 -valued total Function holds
( y in the carrier of () & 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 b1 -valued total Function holds
( y in the carrier of () & 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 () & 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 () & y . q in the carrier of G & y = q .--> (y . q) )

A2: q in {q} by TARSKI:def 1;
A3: the carrier of () = product () by GROUP_7:def 2;
ex R being 1-sorted st
( R = F . q & () . q = the carrier of R ) by ;
then A4: (Carrier F) . q = the carrier of G by ;
A5: dom () = {q} by PARTFUN1:def 2;
let y be {q} -defined the carrier of G -valued total Function; :: thesis: ( y in the carrier of () & 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 ;
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 () . i
let i be object ; :: thesis: ( i in dom y implies y . i in () . i )
assume A8: i in dom y ; :: thesis: y . i in () . i
then A9: i = q by TARSKI:def 1;
y . i = z by ;
hence y . i in () . i by A4, A9; :: thesis: verum
end;
hence ( y in the carrier of () & y . q in the carrier of G & y = q .--> (y . q) ) by ; :: thesis: verum