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

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

then X . n = {} by FUNCT_1:def 2;
hence X . n is Subset of A by XBOOLE_1:2; :: thesis: verum

end;

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

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

end;

end;