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

now :: thesis: for y being object holds
( ( y in { (f .: x) where x is Element of X : verum } implies ex x being object st
( x in dom ((.: f) | X) & y = ((.: f) | X) . x ) ) & ( ex x being object st
( x in dom ((.: f) | X) & y = ((.: f) | X) . x ) implies y in { (f .: x) where x is Element of X : verum } ) )

let y be object ; :: thesis: ( ( y in { (f .: x) where x is Element of X : verum } implies ex x being object st
( x in dom ((.: f) | X) & y = ((.: f) | X) . x ) ) & ( ex x being object st
( x in dom ((.: f) | X) & y = ((.: f) | X) . x ) implies y in { (f .: x) where x is Element of X : verum } ) )

hereby :: thesis: ( ex x being object st
( x in dom ((.: f) | X) & y = ((.: f) | X) . x ) implies y in { (f .: x) where x is Element of X : verum } )

assume y in { (f .: x) where x is Element of X : verum } ; :: thesis: ex x being object st
( x in dom ((.: f) | X) & y = ((.: f) | X) . x )
then consider x9 being Element of X such that
A1: y = f .: x9 ;
reconsider x = x9 as object ;
take x = x; :: thesis: ( x in dom ((.: f) | X) & y = ((.: f) | X) . x )
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: y = ((.: f) | X) . x
thus y = (.: f) . x by A1, A2, FUNCT_3:7
.= ((.: f) | X) . x by FUNCT_1:49 ; :: thesis: verum

end;

given x being object such that A3: ( x in dom ((.: f) | X) & y = ((.: f) | X) . x ) ; :: thesis: y in { (f .: x) where x is Element of X : verum }
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: verum

end;

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