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;