let D be non empty set ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: FinS ((max+ F),X) = FinS (F,X)

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

let d be Element of D; :: thesis: ( d in dom (F | X) implies (F | X) . d >= 0 )
assume A3: d in dom (F | X) ; :: thesis: (F | X) . d >= 0
then F . d >= 0 by A2;
hence (F | X) . d >= 0 by A3, FUNCT_1:47; :: thesis: verum

end;

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 ;
:: thesis: verum