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 )

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

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

f /. c = d ) :: 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() )

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 A5: c in dom (f | X) ; :: thesis: (f | X) . c = d

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

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

thus (f | X) . c = f . c by A5, FUNCT_1:47

.= f /. c by A7, PARTFUN1:def 6

.= d by A4, A6 ; :: 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 )

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

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

f /. c = d ) :: 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() )

proof

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

(f | X) . c = d ; :: according to PARTFUN2:def 1 :: thesis: ex d being Element of D st

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

f /. c = d

take 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 A3: c in dom (f | X) by RELAT_1:61;

c in dom f by A2, XBOOLE_0:def 4;

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

.= (f | X) . c by A3, FUNCT_1:47

.= d by A1, A3 ;

:: thesis: verum

end;(f | X) . c = d ; :: according to PARTFUN2:def 1 :: thesis: ex d being Element of D st

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

f /. c = d

take 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 A3: c in dom (f | X) by RELAT_1:61;

c in dom f by A2, XBOOLE_0:def 4;

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

.= (f | X) . c by A3, FUNCT_1:47

.= d by A1, A3 ;

:: 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 A5: c in dom (f | X) ; :: thesis: (f | X) . c = d

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

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

thus (f | X) . c = f . c by A5, FUNCT_1:47

.= f /. c by A7, PARTFUN1:def 6

.= d by A4, A6 ; :: thesis: verum