consider n being Nat such that
A1: for x being object st x in rng M holds
ex s being FinSequence st
( s = x & len s = n ) by Def1;
hereby :: thesis: ( ( 0 = len M or 0 = width M ) implies M is empty-yielding )
set s = the Element of rng M;
assume A2: M is empty-yielding ; :: thesis: ( 0 <> len M implies 0 = width M )
assume A3: 0 <> len M ; :: thesis: 0 = width M
then A4: M <> {} ;
then ex p being FinSequence st
( p = the Element of rng M & len p = n ) by A1;
then reconsider s = the Element of rng M as FinSequence ;
s = 0 by A2, A4, RELAT_1:149;
then len s = 0 ;
hence 0 = width M by A3, A4, Def3; :: thesis: verum
end;
assume A5: ( 0 = len M or 0 = width M ) ; :: thesis: M is empty-yielding
now :: thesis: for s being set st s in rng M holds
s = {}
let s be set ; :: thesis: ( s in rng M implies s = {} )
assume A6: s in rng M ; :: thesis: s = {}
then M <> {} ;
then len M > 0 ;
then consider p being FinSequence such that
A7: p in rng M and
A8: len p = 0 by A5, Def3;
ex q being FinSequence st
( q = p & len q = n ) by A1, A7;
then ex q being FinSequence st
( q = s & len q = 0 ) by A1, A6, A8;
hence s = {} ; :: thesis: verum
end;
hence M is empty-yielding by RELAT_1:149; :: thesis: verum