let C be non empty set ; :: thesis: for f being PartFunc of C,ExtREAL holds f = (max+ f) - (max- f)

let f be PartFunc of C,ExtREAL; :: thesis: f = (max+ f) - (max- f)

A1: dom f = dom ((max+ f) - (max- f)) by Th17;

for x being Element of C st x in dom f holds

f . x = ((max+ f) - (max- f)) . x

let f be PartFunc of C,ExtREAL; :: thesis: f = (max+ f) - (max- f)

A1: dom f = dom ((max+ f) - (max- f)) by Th17;

for x being Element of C st x in dom f holds

f . x = ((max+ f) - (max- f)) . x

proof

hence
f = (max+ f) - (max- f)
by A1, PARTFUN1:5; :: thesis: verum
let x be Element of C; :: thesis: ( x in dom f implies f . x = ((max+ f) - (max- f)) . x )

assume A2: x in dom f ; :: thesis: f . x = ((max+ f) - (max- f)) . x

then A3: ((max+ f) - (max- f)) . x = ((max+ f) . x) - ((max- f) . x) by A1, MESFUNC1:def 4;

end;assume A2: x in dom f ; :: thesis: f . x = ((max+ f) - (max- f)) . x

then A3: ((max+ f) - (max- f)) . x = ((max+ f) . x) - ((max- f) . x) by A1, MESFUNC1:def 4;