let I be non empty finite set ; :: thesis: for F being Group-like associative 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 Group-like associative 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

D1: dom (Carrier F) = I by PARTFUN1:def 2;

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

then consider f being Function such that

D2: ( x = f & dom f = dom (Carrier F) & ( for y being object st y in dom (Carrier F) holds

f . y in (Carrier F) . y ) ) by CARD_3:def 5, A1;

thus x is I -defined total Function by D2, D1, RELAT_1:def 18, PARTFUN1:def 2; :: thesis: verum

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

x is I -defined total Function

let F be Group-like associative 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

D1: dom (Carrier F) = I by PARTFUN1:def 2;

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

then consider f being Function such that

D2: ( x = f & dom f = dom (Carrier F) & ( for y being object st y in dom (Carrier F) holds

f . y in (Carrier F) . y ) ) by CARD_3:def 5, A1;

thus x is I -defined total Function by D2, D1, RELAT_1:def 18, PARTFUN1:def 2; :: thesis: verum