let n1, n2 be Nat; :: thesis: ( ( len M > 0 & ex s being FinSequence st
( s in rng M & len s = n1 ) & ex s being FinSequence st
( s in rng M & len s = n2 ) implies n1 = n2 ) & ( not len M > 0 & n1 = 0 & n2 = 0 implies n1 = n2 ) )
thus ( len M > 0 & ex s being FinSequence st
( s in rng M & len s = n1 ) & ex s being FinSequence st
( s in rng M & len s = n2 ) implies n1 = n2 ) :: thesis: ( not len M > 0 & n1 = 0 & n2 = 0 implies n1 = n2 )

proof

assume len M > 0 ; :: thesis: ( for s being FinSequence holds
( not s in rng M or not len s = n1 ) or for s being FinSequence holds
( not s in rng M or not len s = n2 ) or n1 = n2 )
given s being FinSequence such that A4: s in rng M and
A5: len s = n1 ; :: thesis: ( for s being FinSequence holds
( not s in rng M or not len s = n2 ) or n1 = n2 )
consider n being Nat such that
A6: for x being object st x in rng M holds
ex s being FinSequence st
( s = x & len s = n ) by Def1;
A7: ex s1 being FinSequence st
( s1 = s & len s1 = n ) by A6, A4;
given p being FinSequence such that A8: p in rng M and
A9: len p = n2 ; :: thesis: n1 = n2
ex p1 being FinSequence st
( p1 = p & len p1 = n ) by A6, A8;
hence n1 = n2 by A5, A9, A7; :: thesis: verum

end;

thus ( not len M > 0 & n1 = 0 & n2 = 0 implies n1 = n2 ) ; :: thesis: verum