let X be non empty set ; for f being PartFunc of X,ExtREAL
for A being set holds |.f.| | A = |.(f | A).|
let f be PartFunc of X,ExtREAL; for A being set holds |.f.| | A = |.(f | A).|
let A be set ; |.f.| | A = |.(f | A).|
dom (|.f.| | A) = (dom |.f.|) /\ A
by RELAT_1:61;
then A1:
dom (|.f.| | A) = (dom f) /\ A
by MESFUNC1:def 10;
A2:
dom (f | A) = (dom f) /\ A
by RELAT_1:61;
then A3:
dom |.(f | A).| = (dom f) /\ A
by MESFUNC1:def 10;
now for x being Element of X st x in dom (|.f.| | A) holds
(|.f.| | A) . x = |.(f | A).| . xlet x be
Element of
X;
( x in dom (|.f.| | A) implies (|.f.| | A) . x = |.(f | A).| . x )assume A4:
x in dom (|.f.| | A)
;
(|.f.| | A) . x = |.(f | A).| . xthen
|.(f | A).| . x = |.((f | A) . x).|
by A1, A3, MESFUNC1:def 10;
then A5:
|.(f | A).| . x = |.(f . x).|
by A2, A1, A4, FUNCT_1:47;
x in dom f
by A1, A4, XBOOLE_0:def 4;
then A6:
x in dom |.f.|
by MESFUNC1:def 10;
(|.f.| | A) . x = |.f.| . x
by A4, FUNCT_1:47;
hence
(|.f.| | A) . x = |.(f | A).| . x
by A6, A5, MESFUNC1:def 10;
verum end;
hence
|.f.| | A = |.(f | A).|
by A1, A3, PARTFUN1:5; verum