defpred S₁[ object ] means ex f being finite Function st
( f in A & $1 in dom f );
consider X being set such that
A1: for x being object holds
( x in X iff ( x in V & S₁[x] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: for x being object holds
( x in X iff ex f being finite Function st
( f in A & x in dom f ) )
let x be object ; :: thesis: ( x in X iff ex f being finite Function st
( f in A & x in dom f ) )
thus ( x in X implies ex f being finite Function st
( f in A & x in dom f ) ) by A1; :: thesis: ( ex f being finite Function st
( f in A & x in dom f ) implies x in X )
given f being finite Function such that A2: f in A and
A3: x in dom f ; :: thesis: x in X
A c= PFuncs (V,C) by FINSUB_1:def 5;
then ex f1 being Function st
( f = f1 & dom f1 c= V & rng f1 c= C ) by A2, PARTFUN1:def 3;
hence x in X by A1, A2, A3; :: thesis: verum