let D be non empty set ; 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; ( 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;
hence
F = (max+ F) - (max- F)
by A4, PARTFUN1:5; ( 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;
hence
abs F = (max+ F) + (max- F)
by A7, PARTFUN1:5; 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;
hence
2 (#) (max+ F) = F + (abs F)
by A2, A9, A10, PARTFUN1:5; verum