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