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