defpred S₂[ object ] means ex g being Function st
( $1 = g & dom g c= dom f & ( for x being object st x in dom g holds
g . x in f . x ) );
let A, B be set ; :: thesis: ( ( for x being object holds
( x in A iff ex g being Function st
( x = g & dom g c= dom f & ( for x being object st x in dom g holds
g . x in f . x ) ) ) ) & ( for x being object holds
( x in B iff ex g being Function st
( x = g & dom g c= dom f & ( for x being object st x in dom g holds
g . x in f . x ) ) ) ) implies A = B )
assume that
A8: for x being object holds
( x in A iff S₂[x] ) and
A9: for x being object holds
( x in B iff S₂[x] ) ; :: thesis: A = B
thus A = B from XBOOLE_0:sch 2(A8, A9); :: thesis: verum