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 (max+ F) = dom F by Def10;
B1: dom (max- F) = dom F by Def11;
C1: ( dom (abs F) = dom F & dom (2 (#) (max+ F)) = dom (max+ F) ) by VALUED_1:def 5, VALUED_1:def 11;
X: dom F = (dom F) /\ (dom F) ;
dom (- (max- F)) = dom (max- F) by VALUED_1:def 5;
then A2: dom F = dom ((max+ F) + (- (max- F))) by X, A1, B1, VALUED_1:def 1;
B2: ( dom (abs F) = dom ((max+ F) + (max- F)) & dom (2 (#) (max+ F)) = dom (F + (abs F)) ) by X, A1, C1, B1, VALUED_1:def 1;

now

let d be Element of D; :: thesis: ( d in dom F implies ((max+ F) - (max- F)) . d = F . d )
assume A3: 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 A2, VALUED_1:13
.= (max+ (F . d)) - ((max- F) . d) by A1, A3, Def10
.= (max+ (F . d)) - (max- (F . d)) by B1, A3, Def11
.= F . d by Th1 ;
:: thesis: verum

end;

hence F = (max+ F) - (max- F) by A2, PARTFUN1:34; :: thesis: ( abs F = (max+ F) + (max- F) & 2 (#) (max+ F) = F + (abs F) )

now

let d be Element of D; :: thesis: ( d in dom (abs F) implies ((max+ F) + (max- F)) . d = (abs F) . d )
assume A4: 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 B2, VALUED_1:def 1
.= (max+ (F . d)) + ((max- F) . d) by A1, C1, A4, Def10
.= (max+ (F . d)) + (max- (F . d)) by C1, B1, A4, Def11
.= abs (F . d) by Th2
.= (abs F) . d by VALUED_1:18 ;
:: thesis: verum

end;

hence abs F = (max+ F) + (max- F) by B2, PARTFUN1:34; :: thesis: 2 (#) (max+ F) = F + (abs F)

now

let d be Element of D; :: thesis: ( d in dom F implies (2 (#) (max+ F)) . d = (F + (abs F)) . d )
assume A5: d in dom F ; :: thesis: (2 (#) (max+ F)) . d = (F + (abs F)) . d
hence (2 (#) (max+ F)) . d = 2 * ((max+ F) . d) by A1, C1, VALUED_1:def 5
.= 2 * (max+ (F . d)) by A1, A5, Def10
.= (F . d) + (abs (F . d)) by Th3
.= (F . d) + ((abs F) . d) by VALUED_1:18
.= (F + (abs F)) . d by A1, C1, B2, A5, VALUED_1:def 1 ;
:: thesis: verum

end;

hence 2 (#) (max+ F) = F + (abs F) by A1, C1, B2, PARTFUN1:34; :: thesis: verum