theorem :: FINSUB_1:11

for A, B being set holds Fin (A /\ B) = (Fin A) /\ (Fin B)