let X be set ; :: thesis: for C, D being non empty set

for f being PartFunc of C,D st X misses dom f holds

f | X is V8()

let C, D be non empty set ; :: thesis: for f being PartFunc of C,D st X misses dom f holds

f | X is V8()

let f be PartFunc of C,D; :: thesis: ( X misses dom f implies f | X is V8() )

assume A1: X /\ (dom f) = {} ; :: according to XBOOLE_0:def 7 :: thesis: f | X is V8()

for f being PartFunc of C,D st X misses dom f holds

f | X is V8()

let C, D be non empty set ; :: thesis: for f being PartFunc of C,D st X misses dom f holds

f | X is V8()

let f be PartFunc of C,D; :: thesis: ( X misses dom f implies f | X is V8() )

assume A1: X /\ (dom f) = {} ; :: according to XBOOLE_0:def 7 :: thesis: f | X is V8()

now :: thesis: ex d being Element of D st

for c being Element of C st c in X /\ (dom f) holds

f /. c = d

hence
f | X is V8()
by Th35; :: thesis: verumfor c being Element of C st c in X /\ (dom f) holds

f /. c = d

set d = the Element of D;

take d = the Element of D; :: thesis: for c being Element of C st c in X /\ (dom f) holds

f /. c = d

let c be Element of C; :: thesis: ( c in X /\ (dom f) implies f /. c = d )

thus ( c in X /\ (dom f) implies f /. c = d ) by A1; :: thesis: verum

end;take d = the Element of D; :: thesis: for c being Element of C st c in X /\ (dom f) holds

f /. c = d

let c be Element of C; :: thesis: ( c in X /\ (dom f) implies f /. c = d )

thus ( c in X /\ (dom f) implies f /. c = d ) by A1; :: thesis: verum