set D = the non empty Element of W;
deffunc H1( set ) -> non empty Element of W = the non empty Element of W;
consider L being Sequence such that
A1: ( dom L = On W & ( for A being Ordinal
for L1 being Sequence st A in On W & L1 = L | A holds
L . A = H1(L1) ) ) from ORDINAL1:sch 4();
 rng L c= W
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng L or x in W )
assume x in rng L ; :: thesis: x in W
then consider y being object such that
A2: y in dom L and
A3: x = L . y by FUNCT_1:def 3;
reconsider y = y as Ordinal by A2;
L | y = L | y ;
then x = the non empty Element of W by A1, A2, A3;
hence x in W ; :: thesis: verum
end;
then reconsider L = L as Sequence of W by RELAT_1:def 19;
take L ; :: thesis: ( L is DOMAIN-yielding & L is non-empty )
thus dom L = On W by A1; :: according to ZF_REFLE:def 2 :: thesis: L is non-empty
assume {} in rng L ; :: according to RELAT_1:def 9 :: thesis: contradiction
then consider x being object such that
A4: x in dom L and
A5: {} = L . x by FUNCT_1:def 3;
reconsider x = x as Ordinal by A4;
L | x = L | x ;
hence contradiction by A1, A4, A5; :: thesis: verum