let I be non empty set ; :: thesis: for F being multMagma-Family of I
for x being Element of I holds (Carrier F) . x = [#] (F . x)
let F be multMagma-Family of I; :: thesis: for x being Element of I holds (Carrier F) . x = [#] (F . x)
let x be Element of I; :: thesis: (Carrier F) . x = [#] (F . x)
consider R being 1-sorted such that
A1: R = F . x and
A2: (Carrier F) . x = the carrier of R by PRALG_1:def 13;
thus (Carrier F) . x = [#] (F . x) by A1, A2; :: thesis: verum