let h be Function; :: thesis: for A being set
for x being object st A <> {} & x in dom h holds
dom (h * (A --> x)) <> {}
let A be set ; :: thesis: for x being object st A <> {} & x in dom h holds
dom (h * (A --> x)) <> {}
let x be object ; :: 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)) <> {}
set y = the Element of A;
A3: the Element of A in dom (A --> x) by A1;
(A --> x) . the Element of A = x by A1, Th7;
hence dom (h * (A --> x)) <> {} by A2, A3, FUNCT_1:11; :: thesis: verum