let D be non empty set ; :: thesis: for F being PartFunc of D,REAL
for X being set holds (max- F) | X = max- (F | X)
let F be PartFunc of D,REAL; :: thesis: for X being set holds (max- F) | X = max- (F | X)
let X be set ; :: thesis: (max- F) | X = max- (F | X)
A1: dom ((max- F) | X) = (dom (max- F)) /\ X by RELAT_1:61;
A2: (dom (max- F)) /\ X = (dom F) /\ X by Def11
.= dom (F | X) by RELAT_1:61 ;
A3: dom (F | X) = dom (max- (F | X)) by Def11;

now :: thesis: for d being Element of D st d in dom ((max- F) | X) holds
((max- F) | X) . d = (max- (F | X)) . d

let d be Element of D; :: thesis: ( d in dom ((max- F) | X) implies ((max- F) | X) . d = (max- (F | X)) . d )
assume A4: d in dom ((max- F) | X) ; :: thesis: ((max- F) | X) . d = (max- (F | X)) . d
then A5: d in dom (max- F) by A1, XBOOLE_0:def 4;
thus ((max- F) | X) . d = (max- F) . d by A4, FUNCT_1:47
.= max- (F . d) by A5, Def11
.= max- ((F | X) . d) by A1, A2, A4, FUNCT_1:47
.= (max- (F | X)) . d by A1, A2, A3, A4, Def11 ; :: thesis: verum

end;

hence (max- F) | X = max- (F | X) by A2, A3, PARTFUN1:5, RELAT_1:61; :: thesis: verum