let Y, X be set ; :: thesis: for C, D being non empty set
for f being PartFunc of C,D st f | Y is constant holds
(f | X) | Y is constant
let C, D be non empty set ; :: thesis: for f being PartFunc of C,D st f | Y is constant holds
(f | X) | Y is constant
let f be PartFunc of C,D; :: thesis: ( f | Y is constant implies (f | X) | Y is constant )
assume f | Y is constant ; :: thesis: (f | X) | Y is constant
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 Thx;
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 Z: c in dom ((f | X) | Y) ; :: thesis: ((f | X) | Y) . c = d
then X: c in Y /\ (dom (f | X)) by RELAT_1:90;
then A2: ( c in Y & c in dom (f | X) ) by XBOOLE_0:def 4;
then ( c in Y & c in (dom f) /\ X ) by RELAT_1:90;
then ( c in Y & c in dom f ) by XBOOLE_0:def 4;
then c in Y /\ (dom f) by XBOOLE_0:def 4;
then f /. c = d by A1;
then (f | X) /. c = d by A2, Th32;
then ((f | X) | Y) /. c = d by Th34, X;
hence ((f | X) | Y) . c = d by Z, PARTFUN1:def 8; :: thesis: verum