per cases ( n in dom F1 or not n in dom F1 ) ;

suppose n in dom F1 ; :: thesis: F1 . n is Subset of X

hence F1 . n is Subset of X by FINSEQ_2:11; :: thesis: verum

end;

suppose not n in dom F1 ; :: thesis: F1 . n is Subset of X

then F1 . n = {} by FUNCT_1:def 2;
hence F1 . n is Subset of X by SUBSET_1:1; :: thesis: verum

end;

end;