let Y, X be set ; :: thesis: for f being Function holds (Y | f) .: X = Y /\ (f .: X)
let f be Function; :: thesis: (Y | f) .: X = Y /\ (f .: X)
for y being set holds
( y in (Y | f) .: X iff y in Y /\ (f .: X) )

proof

let y be set ; :: thesis: ( y in (Y | f) .: X iff y in Y /\ (f .: X) )
thus ( y in (Y | f) .: X implies y in Y /\ (f .: X) ) :: thesis: ( y in Y /\ (f .: X) implies y in (Y | f) .: X )

proof

assume y in (Y | f) .: X ; :: thesis: y in Y /\ (f .: X)
then consider x being set such that
A1: x in dom (Y | f) and
A2: x in X and
A3: y = (Y | f) . x by Def12;
A4: y = f . x by A1, A3, Th85;
then A5: y in Y by A1, Th85;
x in dom f by A1, Th85;
then y in f .: X by A2, A4, Def12;
hence y in Y /\ (f .: X) by A5, XBOOLE_0:def 4; :: thesis: verum

end;

assume A6: y in Y /\ (f .: X) ; :: thesis: y in (Y | f) .: X
then y in f .: X by XBOOLE_0:def 4;
then consider x being set such that
A7: x in dom f and
A8: x in X and
A9: y = f . x by Def12;
y in Y by A6, XBOOLE_0:def 4;
then A10: x in dom (Y | f) by A7, A9, Th85;
then (Y | f) . x = f . x by Th85;
hence y in (Y | f) .: X by A8, A9, A10, Def12; :: thesis: verum

end;

hence (Y | f) .: X = Y /\ (f .: X) by TARSKI:1; :: thesis: verum