( ( x in I or x nin I ) & dom S = I ) by PARTFUN1:def 2;
hence S . x is trivial by Def2, FUNCT_1:def 2; :: thesis: verum