thus ( len M > 0 implies ex n being Nat ex s being FinSequence st
( s in rng M & len s = n ) ) :: thesis: ( not len M > 0 implies ex b1 being Nat st b1 = 0 )
proof
set x = the Element of rng M;
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;
reconsider n = n as Nat ;
assume len M > 0 ; :: thesis: ex n being Nat ex s being FinSequence st
( s in rng M & len s = n )
then A2: rng M <> {} by CARD_1:27, RELAT_1:41;
then consider s being FinSequence such that
A3: ( s = the Element of rng M & len s = n ) by A1;
take n ; :: thesis: ex s being FinSequence st
( s in rng M & len s = n )
take s ; :: thesis: ( s in rng M & len s = n )
thus ( s in rng M & len s = n ) by A2, A3; :: thesis: verum
end;
thus ( not len M > 0 implies ex b1 being Nat st b1 = 0 ) ; :: thesis: verum