let D be non empty set ; for F being PartFunc of D,REAL
for X being set st dom (F | X) is finite & ( for d being Element of D st d in dom (F | X) holds
F . d >= 0 ) holds
FinS ((max+ F),X) = FinS (F,X)
let F be PartFunc of D,REAL; for X being set st dom (F | X) is finite & ( for d being Element of D st d in dom (F | X) holds
F . d >= 0 ) holds
FinS ((max+ F),X) = FinS (F,X)
let X be set ; ( dom (F | X) is finite & ( for d being Element of D st d in dom (F | X) holds
F . d >= 0 ) implies FinS ((max+ F),X) = FinS (F,X) )
assume that
A1:
dom (F | X) is finite
and
A2:
for d being Element of D st d in dom (F | X) holds
F . d >= 0
; FinS ((max+ F),X) = FinS (F,X)
then A4: F | X =
max+ (F | X)
by Th46
.=
(max+ F) | X
by Th44
;
hence FinS (F,X) =
FinS (((max+ F) | X),X)
by A1, Th64
.=
FinS ((max+ F),X)
by A1, A4, Th64
;
verum