A1:
dom (G .set (WeightSelector,X)) = (dom G) \/ {WeightSelector}
by GLIB_000:7;
WeightSelector in {WeightSelector}
by TARSKI:def 1;
then
WeightSelector in dom (G .set (WeightSelector,X))
by A1, XBOOLE_0:def 3;
hence
not G .set (WeightSelector,X) is plain
by GLIB_000:def 5, GLIB_000:1, GLIB_003:def 1, ENUMSET1:def 2; verum