let i be set ; :: according to PRE_CIRC:def 3 :: thesis: ( not i in I or (A /\ B) . i is finite )
assume A1: i in I ; :: thesis: (A /\ B) . i is finite
then B . i is finite by PRE_CIRC:def 3;
then (A . i) /\ (B . i) is finite ;
hence (A /\ B) . i is finite by A1, PBOOLE:def 8; :: thesis: verum