let I be non empty set ; :: thesis: for F being Group-Family of I
for g being Element of F
for i being Element of I holds g . i is Element of (F . i)
let F be Group-Family of I; :: thesis: for g being Element of F
for i being Element of I holds g . i is Element of (F . i)
let g be Element of F; :: thesis: for i being Element of I holds g . i is Element of (F . i)
let i be Element of I; :: thesis: g . i is Element of (F . i)
g . i is Element of (Carrier F) . i by PBOOLE:def 14;
hence g . i is Element of (F . i) by Th9; :: thesis: verum