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 Def10
.= dom (F | X) by RELAT_1:61 ;
A3: dom (F | X) = dom (max+ (F | X)) by Def10;

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, Def10
.= max+ ((F | X) . d) by A1, A2, A4, FUNCT_1:47
.= (max+ (F | X)) . d by A1, A2, A3, A4, Def10 ; :: thesis: verum

end;

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