reconsider E = {} as Matrix of 0 ,D by MATRIX_0: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_0:24;
hence S . x is Matrix of len (S . x),D by A2; :: thesis: verum

end;

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

S . x = E by A3, FUNCT_1:def 2;
hence S . x is Matrix of len (S . x),D ; :: thesis: verum

end;

end;