let p be FinSequence; :: thesis: ( rng p <> {} implies 1 in dom p )
consider y being Element of rng p;
assume rng p <> {} ; :: thesis: 1 in dom p
then y in rng p ;
hence 1 in dom p by Th33; :: thesis: verum