let D be non empty set ; 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; for X being set holds (max+ F) | X = max+ (F | X)
let X be set ; (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 for d being Element of D st d in dom ((max+ F) | X) holds
((max+ F) | X) . d = (max+ (F | X)) . dlet d be
Element of
D;
( d in dom ((max+ F) | X) implies ((max+ F) | X) . d = (max+ (F | X)) . d )assume A4:
d in dom ((max+ F) | X)
;
((max+ F) | X) . d = (max+ (F | X)) . dthen 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
;
verum end;
hence
(max+ F) | X = max+ (F | X)
by A2, A3, PARTFUN1:5, RELAT_1:61; verum