theorem Def4: :: GROUP_23:18

for I being non empty set
for F being Group-Family of I
for IT being Subgroup-Family of F holds
( IT is componentwise_strict iff for i being Element of I holds IT . i is strict Subgroup of F . i ) ;