per cases ( i in dom A or not i in dom A ) ;

suppose i in dom A ; :: thesis: A . i is finite

then A . i in bool F by PARTFUN1:4;
hence A . i is finite ; :: thesis: verum

end;

suppose not i in dom A ; :: thesis: A . i is finite

hence A . i is finite by FUNCT_1:def 2; :: thesis: verum

end;

end;