let f be non empty one-to-one Function; :: thesis:
let X be non empty Subset of (bool (dom f)); :: thesis:
set S = { (f .: x) where x is Element of X : verum } ;

now :: thesis:

let y be object ; :: thesis:

hereby :: thesis:

assume y in { (f .: x) where x is Element of X : verum } ; :: thesis:
then consider x9 being Element of X such that
A1: y = f .: x9 ;
reconsider x = x9 as object ;
take x = x; :: thesis:
x in bool (dom f) ;
then A2: x in dom (.: f) by FUNCT_3:def 1;
hence x in dom ((.: f) | X) by RELAT_1:57; :: thesis:
thus y = (.: f) . x by A1, A2, FUNCT_3:7
.= ((.: f) | X) . x by FUNCT_1:49 ; :: thesis:

end;

given x being object such that A3: ( x in dom ((.: f) | X) & y = ((.: f) | X) . x ) ; :: thesis:
A4: ( x in dom (.: f) & x in X ) by A3, RELAT_1:57;
then reconsider x9 = x as Element of X ;
y = (.: f) . x by A3, FUNCT_1:47
.= f .: x9 by A4, FUNCT_3:7 ;
hence y in { (f .: x) where x is Element of X : verum } ; :: thesis:

end;

hence rng ((.: f) | X) = { (f .: x) where x is Element of X : verum } by FUNCT_1:def 3; :: thesis: