set phi = (On W) --> {} ;
A1: ( dom ((On W) --> {} ) = On W & ( for A being Ordinal st A in On W holds
((On W) --> {} ) . A = {} ) ) by FUNCOP_1:13, FUNCOP_1:19;
A2: rng ((On W) --> {} ) c= {{} } by FUNCOP_1:19;
reconsider phi = (On W) --> {} as Ordinal-Sequence ;
take phi ; :: thesis: ( dom phi = On W & rng phi c= On W )
thus dom phi = On W by FUNCOP_1:19; :: thesis: rng phi c= On W
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng phi or x in On W )
assume A3: x in rng phi ; :: thesis: x in On W
then A4: dom phi <> {} by RELAT_1:65;
x = {} by A2, A3, TARSKI:def 1;
hence x in On W by A1, A4, ORDINAL3:10; :: thesis: verum