let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL
for A being set holds |.f.| | A = |.(f | A).|
let f be PartFunc of X,ExtREAL ; :: thesis: for A being set holds |.f.| | A = |.(f | A).|
let A be set ; :: thesis: |.f.| | A = |.(f | A).|
A1: ( dom (|.f.| | A) = (dom |.f.|) /\ A & dom (f | A) = (dom f) /\ A ) by RELAT_1:90;
then A2: ( dom (|.f.| | A) = (dom f) /\ A & dom |.(f | A).| = (dom f) /\ A ) by MESFUNC1:def 10;

now

let x be Element of X; :: thesis: ( x in dom (|.f.| | A) implies (|.f.| | A) . x = |.(f | A).| . x )
assume A3: x in dom (|.f.| | A) ; :: thesis: (|.f.| | A) . x = |.(f | A).| . x
then A4: (|.f.| | A) . x = |.f.| . x by FUNCT_1:70;
x in dom f by A2, A3, XBOOLE_0:def 4;
then A5: x in dom |.f.| by MESFUNC1:def 10;
|.(f | A).| . x = |.((f | A) . x).| by A2, A3, MESFUNC1:def 10;
then |.(f | A).| . x = |.(f . x).| by A1, A2, A3, FUNCT_1:70;
hence (|.f.| | A) . x = |.(f | A).| . x by A4, A5, MESFUNC1:def 10; :: thesis: verum

end;

hence |.f.| | A = |.(f | A).| by A2, PARTFUN1:34; :: thesis: verum