let p be FinSequence; :: thesis: ( rng p <> {} implies 1 in dom p )
set y = the Element of rng p;
assume rng p <> {} ; :: thesis: 1 in dom p
then the Element of rng p in rng p ;
hence 1 in dom p by Th29; :: thesis: verum