a in On W by ORDINAL1:def 10;
then a in dom L by Def5;
then A4: L . a in rng L by FUNCT_1:def 5;
rng L c= W by RELAT_1:def 19;
hence L . a is non empty Element of W by A4, RELAT_1:def 9; :: thesis: verum