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

suppose i in dom F ; :: thesis: F . i is PartFunc of A,B

then A1: F . i in rng F by FUNCT_1:def 3;
rng F c= PFuncs (A,B) by RELAT_1:def 19;
hence F . i is PartFunc of A,B by A1, Th46; :: thesis: verum

end;

suppose not i in dom F ; :: thesis: F . i is PartFunc of A,B

then F . i = {} by FUNCT_1:def 2;
hence F . i is PartFunc of A,B by RELSET_1:12; :: thesis: verum

end;

end;