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