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

for f being PartFunc of C,D holds

( f | X is V8() iff ex d being Element of D st

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

f . c = d )

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

( f | X is V8() iff ex d being Element of D st

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

f . c = d )

let f be PartFunc of C,D; :: thesis: ( f | X is V8() iff ex d being Element of D st

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

f . c = d )

f . c = d ; :: thesis: f | X is V8()

take d ; :: according to PARTFUN2:def 1 :: thesis: for c being Element of C st c in dom (f | X) holds

(f | X) . c = d

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

assume A4: c in dom (f | X) ; :: thesis: (f | X) . c = d

then A5: c in X /\ (dom f) by RELAT_1:61;

then A6: c in dom f by XBOOLE_0:def 4;

thus (f | X) . c = (f | X) /. c by A4, PARTFUN1:def 6

.= f /. c by A5, Th16

.= f . c by A6, PARTFUN1:def 6

.= d by A3, A5 ; :: thesis: verum

for f being PartFunc of C,D holds

( f | X is V8() iff ex d being Element of D st

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

f . c = d )

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

( f | X is V8() iff ex d being Element of D st

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

f . c = d )

let f be PartFunc of C,D; :: thesis: ( f | X is V8() iff ex d being Element of D st

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

f . c = d )

hereby :: thesis: ( ex d being Element of D st

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

f . c = d implies f | X is V8() )

given d being Element of D such that A3:
for c being Element of C st c in X /\ (dom f) holds for c being Element of C st c in X /\ (dom f) holds

f . c = d implies f | X is V8() )

assume
f | X is V8()
; :: thesis: ex d being Element of D st

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

f . c = d

then consider d being Element of D such that

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

f /. c = d by Th35;

take d = 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 )

assume A2: c in X /\ (dom f) ; :: thesis: f . c = d

then c in dom f by XBOOLE_0:def 4;

hence f . c = f /. c by PARTFUN1:def 6

.= d by A1, A2 ;

:: thesis: verum

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

f . c = d

then consider d being Element of D such that

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

f /. c = d by Th35;

take d = 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 )

assume A2: c in X /\ (dom f) ; :: thesis: f . c = d

then c in dom f by XBOOLE_0:def 4;

hence f . c = f /. c by PARTFUN1:def 6

.= d by A1, A2 ;

:: thesis: verum

f . c = d ; :: thesis: f | X is V8()

take d ; :: according to PARTFUN2:def 1 :: thesis: for c being Element of C st c in dom (f | X) holds

(f | X) . c = d

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

assume A4: c in dom (f | X) ; :: thesis: (f | X) . c = d

then A5: c in X /\ (dom f) by RELAT_1:61;

then A6: c in dom f by XBOOLE_0:def 4;

thus (f | X) . c = (f | X) /. c by A4, PARTFUN1:def 6

.= f /. c by A5, Th16

.= f . c by A6, PARTFUN1:def 6

.= d by A3, A5 ; :: thesis: verum