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

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