let I be non empty set ; :: thesis: for i being Element of I
for F being Group-Family of I holds (Carrier F) . i = the carrier of (F . i)
let i be Element of I; :: thesis: for F being Group-Family of I holds (Carrier F) . i = the carrier of (F . i)
let F be Group-Family of I; :: thesis: (Carrier F) . i = the carrier of (F . i)
ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def 15;
hence (Carrier F) . i = the carrier of (F . i) ; :: thesis: verum