A1: dom f = X by FUNCT_2:def 1;

per cases ( x in X or not x in X ) ;

suppose x in X ; :: thesis: f . x is finite Subset of Y

then f . x in Fin Y by FUNCT_2:5;
hence f . x is finite Subset of Y by FINSUB_1:def 5; :: thesis: verum

end;

suppose not x in X ; :: thesis: f . x is finite Subset of Y

then f . x = {} by A1, FUNCT_1:def 2;
hence f . x is finite Subset of Y by XBOOLE_1:2; :: thesis: verum

end;

end;