let X be non empty set ; :: thesis: for f, g being PartFunc of X,REAL holds
( dom ((max+ (f + g)) + (max- f)) = (dom f) /\ (dom g) & dom ((max- (f + g)) + (max+ f)) = (dom f) /\ (dom g) & dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) & dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) & (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative )
let f, g be PartFunc of X,REAL; :: thesis: ( dom ((max+ (f + g)) + (max- f)) = (dom f) /\ (dom g) & dom ((max- (f + g)) + (max+ f)) = (dom f) /\ (dom g) & dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) & dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) & (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative )
A1: ( dom (max- f) = dom f & dom ((max+ (f + g)) + (max- f)) = (dom (max+ (f + g))) /\ (dom (max- f)) ) by RFUNCT_3:def 11, VALUED_1:def 1;
A2: ( dom (max+ f) = dom f & dom ((max- (f + g)) + (max+ f)) = (dom (max- (f + g))) /\ (dom (max+ f)) ) by RFUNCT_3:def 10, VALUED_1:def 1;
A3: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;
then A4: dom (max- (f + g)) = (dom f) /\ (dom g) by RFUNCT_3:def 11;
dom (max+ (f + g)) = (dom f) /\ (dom g) by A3, RFUNCT_3:def 10;
then A5: dom ((max+ (f + g)) + (max- f)) = (dom g) /\ ((dom f) /\ (dom f)) by A1, XBOOLE_1:16;
hence ( dom ((max+ (f + g)) + (max- f)) = (dom f) /\ (dom g) & dom ((max- (f + g)) + (max+ f)) = (dom f) /\ (dom g) ) by A4, A2, XBOOLE_1:16; :: thesis: ( dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) & dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) & (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative )
dom (max- g) = dom g by RFUNCT_3:def 11;
then dom (((max+ (f + g)) + (max- f)) + (max- g)) = ((dom f) /\ (dom g)) /\ (dom g) by A5, VALUED_1:def 1
.= (dom f) /\ ((dom g) /\ (dom g)) by XBOOLE_1:16 ;
hence dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) ; :: thesis: ( dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) & (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative )
( dom (max+ g) = dom g & dom ((max- (f + g)) + (max+ f)) = (dom g) /\ ((dom f) /\ (dom f)) ) by A4, A2, RFUNCT_3:def 10, XBOOLE_1:16;
then dom (((max- (f + g)) + (max+ f)) + (max+ g)) = ((dom f) /\ (dom g)) /\ (dom g) by VALUED_1:def 1;
then dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ ((dom g) /\ (dom g)) by XBOOLE_1:16;
hence dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) ; :: thesis: ( (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative )
now :: thesis: for x being object st x in dom ((max+ (f + g)) + (max- f)) holds
0 <= ((max+ (f + g)) + (max- f)) . x
let x be object ; :: thesis: ( x in dom ((max+ (f + g)) + (max- f)) implies 0 <= ((max+ (f + g)) + (max- f)) . x )
assume A6: x in dom ((max+ (f + g)) + (max- f)) ; :: thesis: 0 <= ((max+ (f + g)) + (max- f)) . x
then ( 0 <= (max+ (f + g)) . x & 0 <= (max- f) . x ) by RFUNCT_3:37, RFUNCT_3:40;
then 0 + 0 <= ((max+ (f + g)) . x) + ((max- f) . x) ;
hence 0 <= ((max+ (f + g)) + (max- f)) . x by A6, VALUED_1:def 1; :: thesis: verum
end;
hence (max+ (f + g)) + (max- f) is nonnegative by Th52; :: thesis: (max- (f + g)) + (max+ f) is nonnegative
now :: thesis: for x being object st x in dom ((max- (f + g)) + (max+ f)) holds
0 <= ((max- (f + g)) + (max+ f)) . x
let x be object ; :: thesis: ( x in dom ((max- (f + g)) + (max+ f)) implies 0 <= ((max- (f + g)) + (max+ f)) . x )
assume A7: x in dom ((max- (f + g)) + (max+ f)) ; :: thesis: 0 <= ((max- (f + g)) + (max+ f)) . x
then ( 0 <= (max- (f + g)) . x & 0 <= (max+ f) . x ) by RFUNCT_3:37, RFUNCT_3:40;
then 0 + 0 <= ((max- (f + g)) . x) + ((max+ f) . x) ;
hence 0 <= ((max- (f + g)) + (max+ f)) . x by A7, VALUED_1:def 1; :: thesis: verum
end;
hence (max- (f + g)) + (max+ f) is nonnegative by Th52; :: thesis: verum