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 ;
A5: dom (f | B) = (dom f) /\ B by RELAT_1:61;
then y in B by ;
then A6: y in C /\ B by ;
y in dom f by ;
hence x in f .: (C /\ B) by ; :: 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 ;
y in B by ;
then y in (dom f) /\ B by ;
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 ; :: thesis: verum