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

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

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

end;

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

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

end;

end;