let X, Y be set ; 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 ; 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; ( f | Y is V8() implies (f | X) | Y is V8() )
assume
f | Y is V8()
; (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
; PARTFUN2:def 1 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; ( c in dom ((f | X) | Y) implies ((f | X) | Y) . c = d )
assume A2:
c in dom ((f | X) | Y)
; ((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; verum