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

suppose A1: x in dom F ; :: thesis: F . x is Matrix of D

thus F . x is Matrix of D by A1, Def2; :: thesis: verum

end;

suppose not x in dom F ; :: thesis: F . x is Matrix of D

then F . x = {} by FUNCT_1:def 2;
hence F . x is Matrix of D by MATRIX_0:13; :: thesis: verum

end;

end;