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 A1: ( dom (F | X) is finite & ( 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

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

end;

then A2: F | X = max+ (F | X) by Th49
.= (max+ F) | X by Th47 ;
hence FinS F,X = FinS ((max+ F) | X),X by A1, Th67
.= FinS (max+ F),X by A1, A2, Th67 ;
:: thesis: verum