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;

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

hence
|.f.| | A = |.(f | A).|
by A1, A3, PARTFUN1:5; :: thesis: verum(|.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;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