defpred S₁[ object ] means ( $1 in dom f & f /. $1 <> 0. X );
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 <> 0. X ) )
let x be object ; :: thesis: ( x in A iff ( x in dom f & f /. x <> 0. X ) )
thus ( x in A implies ( x in dom f & f /. x <> 0. X ) ) by A1; :: thesis: ( x in dom f & f /. x <> 0. X implies x in A )
assume ( x in dom f & f /. x <> 0. X ) ; :: thesis: x in A
hence x in A by A1; :: thesis: verum