set s = the Element of D;
1 in dom the Element of D by FINSEQ_5:6;
then the Element of D . 1 in rng the Element of D by FUNCT_1:3;
hence ex b₁ being Element of S ex s being Element of D st b₁ in rng s ; :: thesis: verum