consider A being set such that
A1: for x being object holds
( x in A iff ( x in dom f & S₁[x] ) ) from XBOOLE_0:sch 1();
take A ; :: thesis: for x being object holds
( x in A iff ( x in dom f & f . x < a ) )
thus for x being object holds
( x in A iff ( x in dom f & f . x < a ) ) by A1; :: thesis: verum