defpred S₁[ object ] means ex j being set st
( j in J & j in dom A & $1 in A . j );
consider X being set such that
A1: for x being object holds
( x in X iff ( x in F & S₁[x] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: for x being object holds
( x in X iff ex j being set st
( j in J & j in dom A & x in A . j ) )
let x be object ; :: thesis: ( x in X iff ex j being set st
( j in J & j in dom A & x in A . j ) )
thus ( x in X implies ex j being set st
( j in J & j in dom A & x in A . j ) ) by A1; :: thesis: ( ex j being set st
( j in J & j in dom A & x in A . j ) implies x in X )
given j being set such that A2: j in J and
A3: j in dom A and
A4: x in A . j ; :: thesis: x in X
( rng A c= bool F & A . j in rng A ) by A3, FINSEQ_1:def 4, FUNCT_1:3;
hence x in X by A1, A2, A3, A4; :: thesis: verum