let X be non empty set ; :: thesis: for f being PartFunc of X,COMPLEX
for A being set holds |.f.| | A = |.(f | A).|
let f be PartFunc of X,COMPLEX; :: thesis: for A being set holds |.f.| | A = |.(f | A).|
let A be set ; :: thesis: |.f.| | A = |.(f | A).|
dom (|.f.| | A) = (dom |.f.|) /\ A by RELAT_1:61;
then A1: dom (|.f.| | A) = (dom f) /\ A by VALUED_1:def 11;
A2: dom (f | A) = (dom f) /\ A by RELAT_1:61;
then A3: dom |.(f | A).| = (dom f) /\ A by VALUED_1:def 11;

now :: thesis: for x being Element of X st x in dom (|.f.| | A) holds
(|.f.| | A) . x = |.(f | A).| . x

let x be Element of X; :: thesis: ( x in dom (|.f.| | A) implies (|.f.| | A) . x = |.(f | A).| . x )
assume A4: x in dom (|.f.| | A) ; :: thesis: (|.f.| | A) . x = |.(f | A).| . x
then |.(f | A).| . x = |.((f | A) . x).| by A1, A3, VALUED_1:def 11;
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 VALUED_1:def 11;
(|.f.| | A) . x = |.f.| . x by A4, FUNCT_1:47;
hence (|.f.| | A) . x = |.(f | A).| . x by A6, A5, VALUED_1:def 11; :: thesis: verum

end;

hence |.f.| | A = |.(f | A).| by A1, A3, PARTFUN1:5; :: thesis: verum