let X, Y 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 object holds
( y in (Y |` f) .: X iff y in Y /\ (f .: X) )

proof

let y be object ; :: 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 object such that
A1: x in dom (Y |` f) and
A2: x in X and
A3: y = (Y |` f) . x by Def6;
A4: y = f . x by A1, A3, Th52;
then A5: y in Y by A1, Th52;
x in dom f by A1, Th52;
then y in f .: X by A2, A4, Def6;
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 object such that
A7: x in dom f and
A8: x in X and
A9: y = f . x by Def6;
y in Y by A6, XBOOLE_0:def 4;
then A10: x in dom (Y |` f) by A7, A9, Th52;
then (Y |` f) . x = f . x by Th52;
hence y in (Y |` f) .: X by A8, A9, A10, Def6; :: thesis: verum

end;

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