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

for f being PartFunc of C,D st f | Y is V8() holds

(f | X) | Y is V8()

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

(f | X) | Y is V8()

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

assume f | Y is V8() ; :: thesis: (f | X) | Y is V8()

then consider d being Element of D such that

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

f /. c = d by Th35;

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

((f | X) | Y) . c = d

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

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

then A3: c in Y /\ (dom (f | X)) by RELAT_1:61;

then A4: c in Y by XBOOLE_0:def 4;

A5: c in dom (f | X) by A3, XBOOLE_0:def 4;

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

then c in dom f by XBOOLE_0:def 4;

then c in Y /\ (dom f) by A4, XBOOLE_0:def 4;

then f /. c = d by A1;

then (f | X) /. c = d by A5, Th15;

then ((f | X) | Y) /. c = d by A3, Th16;

hence ((f | X) | Y) . c = d by A2, PARTFUN1:def 6; :: thesis: verum

for f being PartFunc of C,D st f | Y is V8() holds

(f | X) | Y is V8()

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

(f | X) | Y is V8()

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

assume f | Y is V8() ; :: thesis: (f | X) | Y is V8()

then consider d being Element of D such that

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

f /. c = d by Th35;

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

((f | X) | Y) . c = d

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

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

then A3: c in Y /\ (dom (f | X)) by RELAT_1:61;

then A4: c in Y by XBOOLE_0:def 4;

A5: c in dom (f | X) by A3, XBOOLE_0:def 4;

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

then c in dom f by XBOOLE_0:def 4;

then c in Y /\ (dom f) by A4, XBOOLE_0:def 4;

then f /. c = d by A1;

then (f | X) /. c = d by A5, Th15;

then ((f | X) | Y) /. c = d by A3, Th16;

hence ((f | X) | Y) . c = d by A2, PARTFUN1:def 6; :: thesis: verum