reconsider E = {} as Matrix of 0 , 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),

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

end;

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

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

end;

end;