let I be non empty finite set ; :: thesis: for F being Group-like associative multMagma-Family of I
for x being I -defined total Function st ( for p being Element of I holds x . p in F . p ) holds
x in the carrier of ()

let F be Group-like associative multMagma-Family of I; :: thesis: for x being I -defined total Function st ( for p being Element of I holds x . p in F . p ) holds
x in the carrier of ()

let x be I -defined total Function; :: thesis: ( ( for p being Element of I holds x . p in F . p ) implies x in the carrier of () )
assume A1: for p being Element of I holds x . p in F . p ; :: thesis: x in the carrier of ()
A2: dom () = I by PARTFUN1:def 2;
A3: the carrier of () = product () by GROUP_7:def 2;
A4: dom x = I by PARTFUN1:def 2;
now :: thesis: for i being object st i in dom () holds
x . i in () . i
let i be object ; :: thesis: ( i in dom () implies x . i in () . i )
assume A5: i in dom () ; :: thesis: x . i in () . i
consider R being 1-sorted such that
A6: ( R = F . i & () . i = the carrier of R ) by ;
reconsider i0 = i as Element of I by A5;
x . i0 in the carrier of R by ;
hence x . i in () . i by A6; :: thesis: verum
end;
hence x in the carrier of () by ; :: thesis: verum