let f be Function; :: thesis: for B, C being set holds (f | B) .: C = f .: (C /\ B)
let B, C be set ; :: thesis: (f | B) .: C = f .: (C /\ B)
thus (f | B) .: C c= f .: (C /\ B) :: according to XBOOLE_0:def 10 :: thesis: f .: (C /\ B) c= (f | B) .: C

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (f | B) .: C or x in f .: (C /\ B) )
assume x in (f | B) .: C ; :: thesis: x in f .: (C /\ B)
then consider y being object such that
A1: y in dom (f | B) and
A2: y in C and
A3: x = (f | B) . y by FUNCT_1:def 6;
A4: (f | B) . y = f . y by A1, FUNCT_1:47;
A5: dom (f | B) = (dom f) /\ B by RELAT_1:61;
then y in B by A1, XBOOLE_0:def 4;
then A6: y in C /\ B by A2, XBOOLE_0:def 4;
y in dom f by A1, A5, XBOOLE_0:def 4;
hence x in f .: (C /\ B) by A3, A6, A4, FUNCT_1:def 6; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f .: (C /\ B) or x in (f | B) .: C )
assume x in f .: (C /\ B) ; :: thesis: x in (f | B) .: C
then consider y being object such that
A7: y in dom f and
A8: y in C /\ B and
A9: x = f . y by FUNCT_1:def 6;
A10: y in C by A8, XBOOLE_0:def 4;
y in B by A8, XBOOLE_0:def 4;
then y in (dom f) /\ B by A7, XBOOLE_0:def 4;
then A11: y in dom (f | B) by RELAT_1:61;
then (f | B) . y = f . y by FUNCT_1:47;
hence x in (f | B) .: C by A9, A10, A11, FUNCT_1:def 6; :: thesis: verum