let s be 1-sorted ; :: according to WAYBEL_3:def 7 :: thesis: ( not s in rng (I --> S) or not s is empty )
assume A1: s in rng (I --> S) ; :: thesis: not s is empty
rng (I --> S) c= {S} by FUNCOP_1:19;
hence not s is empty by A1, TARSKI:def 1; :: thesis: verum