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

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

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 .: (C /\ B) or x in (f | B) .: C )
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;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

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