let X be non empty set ; :: thesis: for g being PartFunc of X,REAL
for A being Subset of X holds |.(g | A).| = |.g.| | A
let g be PartFunc of X,REAL; :: thesis: for A being Subset of X holds |.(g | A).| = |.g.| | A
let A be Subset of X; :: thesis: |.(g | A).| = |.g.| | A
reconsider gA = R_EAL (g | A) as PartFunc of X,ExtREAL ;
A1: |.(g | A).| = |.(R_EAL (g | A)).| by MESFUNC5:def 7;
dom |.(g | A).| = dom (g | A) by MESFUNC1:def 10;
then A2: dom |.(g | A).| = (dom g) /\ A by RELAT_1:61;
dom (|.g.| | A) = (dom |.g.|) /\ A by RELAT_1:61;
then A3: dom |.(g | A).| = dom (|.g.| | A) by A2, VALUED_1:def 11;
for x being object st x in dom |.(g | A).| holds
|.(g | A).| . x = (|.g.| | A) . x

proof

let x be object ; :: thesis: ( x in dom |.(g | A).| implies |.(g | A).| . x = (|.g.| | A) . x )
assume A4: x in dom |.(g | A).| ; :: thesis: |.(g | A).| . x = (|.g.| | A) . x
then reconsider x1 = x as Element of X ;
x in dom (g | A) by A4, MESFUNC1:def 10;
then A5: ( x in dom g & x in A ) by RELAT_1:57;
then x in dom (R_EAL g) by MESFUNC5:def 7;
then A6: x in dom |.(R_EAL g).| by MESFUNC1:def 10;
A7: |.(g | A).| . x = |.((R_EAL (g | A)) . x1).| by A4, A1, MESFUNC1:def 10;
(R_EAL (g | A)) . x1 = (g | A) . x1 by MESFUNC5:def 7;
then (R_EAL (g | A)) . x1 = g . x1 by A5, FUNCT_1:49;
then |.((R_EAL (g | A)) . x1).| = |.((R_EAL g) . x1).| by MESFUNC5:def 7;
then |.(g | A).| . x = |.(R_EAL g).| . x1 by A7, A6, MESFUNC1:def 10;
then |.(g | A).| . x = (R_EAL (abs g)) . x1 by MESFUNC6:1;
then |.(g | A).| . x = |.g.| . x1 by MESFUNC5:def 7;
hence |.(g | A).| . x = (|.g.| | A) . x by A5, FUNCT_1:49; :: thesis: verum

end;

hence |.(g | A).| = |.g.| | A by A3, FUNCT_1:2; :: thesis: verum