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

for f being PartFunc of C,D holds f | {x} is V8()

let C, D be non empty set ; :: thesis: for f being PartFunc of C,D holds f | {x} is V8()

let f be PartFunc of C,D; :: thesis: f | {x} is V8()

for f being PartFunc of C,D holds f | {x} is V8()

let C, D be non empty set ; :: thesis: for f being PartFunc of C,D holds f | {x} is V8()

let f be PartFunc of C,D; :: thesis: f | {x} is V8()

now :: thesis: f | {x} is V8()end;

hence
f | {x} is V8()
; :: thesis: verumper cases
( {x} /\ (dom f) = {} or {x} /\ (dom f) <> {} )
;

end;

suppose A1:
{x} /\ (dom f) <> {}
; :: thesis: f | {x} is V8()

set y = the Element of {x} /\ (dom f);

( the Element of {x} /\ (dom f) in {x} & the Element of {x} /\ (dom f) in dom f ) by A1, XBOOLE_0:def 4;

then reconsider x1 = x as Element of C by TARSKI:def 1;

end;( the Element of {x} /\ (dom f) in {x} & the Element of {x} /\ (dom f) in dom f ) by A1, XBOOLE_0:def 4;

then reconsider x1 = x as Element of C by TARSKI:def 1;

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

for c being Element of C st c in {x} /\ (dom f) holds

f /. c = f /. x1

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

f /. c = f /. x1

take d = f /. x1; :: thesis: for c being Element of C st c in {x} /\ (dom f) holds

f /. c = f /. x1

let c be Element of C; :: thesis: ( c in {x} /\ (dom f) implies f /. c = f /. x1 )

assume c in {x} /\ (dom f) ; :: thesis: f /. c = f /. x1

then c in {x} by XBOOLE_0:def 4;

hence f /. c = f /. x1 by TARSKI:def 1; :: thesis: verum

end;f /. c = f /. x1

let c be Element of C; :: thesis: ( c in {x} /\ (dom f) implies f /. c = f /. x1 )

assume c in {x} /\ (dom f) ; :: thesis: f /. c = f /. x1

then c in {x} by XBOOLE_0:def 4;

hence f /. c = f /. x1 by TARSKI:def 1; :: thesis: verum