let I be non empty set ; :: thesis: for F being multMagma-Family of I

for x being set st x in the carrier of (product F) holds

x is I -defined total Function

let F be multMagma-Family of I; :: thesis: for x being set st x in the carrier of (product F) holds

x is I -defined total Function

let x be set ; :: thesis: ( x in the carrier of (product F) implies x is I -defined total Function )

assume A1: x in the carrier of (product F) ; :: thesis: x is I -defined total Function

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

hence x is I -defined total Function by A1; :: thesis: verum

for x being set st x in the carrier of (product F) holds

x is I -defined total Function

let F be multMagma-Family of I; :: thesis: for x being set st x in the carrier of (product F) holds

x is I -defined total Function

let x be set ; :: thesis: ( x in the carrier of (product F) implies x is I -defined total Function )

assume A1: x in the carrier of (product F) ; :: thesis: x is I -defined total Function

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

hence x is I -defined total Function by A1; :: thesis: verum