defpred S₁[ object ] means ex f being finite Function st
( f in A & $1 in dom f );
let r, s be set ; :: thesis: ( ( for x being object holds
( x in r iff ex f being finite Function st
( f in A & x in dom f ) ) ) & ( for x being object holds
( x in s iff ex f being finite Function st
( f in A & x in dom f ) ) ) implies r = s )
assume that
A4: for x being object holds
( x in r iff ex f being finite Function st
( f in A & x in dom f ) ) and
A5: for x being object holds
( x in s iff ex f being finite Function st
( f in A & x in dom f ) ) ; :: thesis: r = s
for X1, X2 being set st ( for x being object holds
( x in X1 iff S₁[x] ) ) & ( for x being object holds
( x in X2 iff S₁[x] ) ) holds
X1 = X2 from XBOOLE_0:sch 3();
hence r = s by A4, A5; :: thesis: verum