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) = () /\ 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 ;
then A5: |.(f | A).| . x = |.(f . x).| by ;
x in dom f by ;
then A6: x in dom |.f.| by VALUED_1:def 11;
(|.f.| | A) . x = |.f.| . x by ;
hence (|.f.| | A) . x = |.(f | A).| . x by ; :: thesis: verum
end;
hence |.f.| | A = |.(f | A).| by ; :: thesis: verum