let h be Function; for A, x being set st A <> {} & x in dom h holds
dom (h * (A --> x)) <> {}
let A, x be set ; ( A <> {} & x in dom h implies dom (h * (A --> x)) <> {} )
assume that
A1:
A <> {}
and
A2:
x in dom h
; dom (h * (A --> x)) <> {}
set y = the Element of A;
the Element of A in A
by A1;
then A3:
the Element of A in dom (A --> x)
by Th19;
(A --> x) . the Element of A = x
by A1, Th13;
hence
dom (h * (A --> x)) <> {}
by A2, A3, FUNCT_1:11; verum