let D be non empty set ; :: thesis: for F being PartFunc of D,REAL holds
( F = (max+ F) - (max- F) & abs F = (max+ F) + (max- F) & 2 (#) (max+ F) = F + (abs F) )
let F be PartFunc of D,REAL; :: thesis: ( F = (max+ F) - (max- F) & abs F = (max+ F) + (max- F) & 2 (#) (max+ F) = F + (abs F) )
A1: dom F = (dom F) /\ (dom F) ;
A2: dom (max+ F) = dom F by Def10;
A3: dom (max- F) = dom F by Def11;
dom (- (max- F)) = dom (max- F) by VALUED_1:def 5;
then A4: dom F = dom ((max+ F) + (- (max- F))) by A2, A3, A1, VALUED_1:def 1;

now :: thesis: for d being Element of D st d in dom F holds
((max+ F) - (max- F)) . d = F . d

let d be Element of D; :: thesis: ( d in dom F implies ((max+ F) - (max- F)) . d = F . d )
assume A5: d in dom F ; :: thesis: ((max+ F) - (max- F)) . d = F . d
hence ((max+ F) - (max- F)) . d = ((max+ F) . d) - ((max- F) . d) by A4, VALUED_1:13
.= (max+ (F . d)) - ((max- F) . d) by A2, A5, Def10
.= (max+ (F . d)) - (max- (F . d)) by A3, A5, Def11
.= F . d by Th1 ;
:: thesis: verum

end;

hence F = (max+ F) - (max- F) by A4, PARTFUN1:5; :: thesis: ( abs F = (max+ F) + (max- F) & 2 (#) (max+ F) = F + (abs F) )
A6: dom (abs F) = dom F by VALUED_1:def 11;
then A7: dom (abs F) = dom ((max+ F) + (max- F)) by A2, A3, A1, VALUED_1:def 1;

now :: thesis: for d being Element of D st d in dom (abs F) holds
((max+ F) + (max- F)) . d = (abs F) . d

let d be Element of D; :: thesis: ( d in dom (abs F) implies ((max+ F) + (max- F)) . d = (abs F) . d )
assume A8: d in dom (abs F) ; :: thesis: ((max+ F) + (max- F)) . d = (abs F) . d
hence ((max+ F) + (max- F)) . d = ((max+ F) . d) + ((max- F) . d) by A7, VALUED_1:def 1
.= (max+ (F . d)) + ((max- F) . d) by A2, A6, A8, Def10
.= (max+ (F . d)) + (max- (F . d)) by A3, A6, A8, Def11
.= |.(F . d).| by Th2
.= (abs F) . d by VALUED_1:18 ;
:: thesis: verum

end;

hence abs F = (max+ F) + (max- F) by A7, PARTFUN1:5; :: thesis: 2 (#) (max+ F) = F + (abs F)
A9: dom (2 (#) (max+ F)) = dom (max+ F) by VALUED_1:def 5;
then A10: dom (2 (#) (max+ F)) = dom (F + (abs F)) by A2, A6, A1, VALUED_1:def 1;

now :: thesis: for d being Element of D st d in dom F holds
(2 (#) (max+ F)) . d = (F + (abs F)) . d

let d be Element of D; :: thesis: ( d in dom F implies (2 (#) (max+ F)) . d = (F + (abs F)) . d )
assume A11: d in dom F ; :: thesis: (2 (#) (max+ F)) . d = (F + (abs F)) . d
hence (2 (#) (max+ F)) . d = 2 * ((max+ F) . d) by A2, A9, VALUED_1:def 5
.= 2 * (max+ (F . d)) by A2, A11, Def10
.= (F . d) + |.(F . d).| by Th3
.= (F . d) + ((abs F) . d) by VALUED_1:18
.= (F + (abs F)) . d by A2, A9, A10, A11, VALUED_1:def 1 ;
:: thesis: verum

end;

hence 2 (#) (max+ F) = F + (abs F) by A2, A9, A10, PARTFUN1:5; :: thesis: verum