reconsider E = {} as Matrix of 0 ,D by MATRIX_1:13;

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

suppose A1: x in dom S ; :: thesis: S . x is Matrix of len (S . x),D

then reconsider i = x as Element of NAT ;
consider n being Nat such that
A2: S . i is Matrix of n,D by A1, Def6;
len (S . i) = n by A2, MATRIX_1:25;
hence S . x is Matrix of len (S . x),D by A2; :: thesis: verum

end;

suppose not x in dom S ; :: thesis: S . x is Matrix of len (S . x),D

then ( S . x = E & len E = 0 ) by FUNCT_1:def 4;
hence S . x is Matrix of len (S . x),D ; :: thesis: verum

end;

end;