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

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

end;

then A4: 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, A4, Th67 ;
:: thesis: verum