for X1, X2 being set st ( for x being object holds

( x in X1 iff S_{1}[x] ) ) & ( for x being object holds

( x in X2 iff S_{1}[x] ) ) holds

X1 = X2 from XBOOLE_0:sch 3();

hence for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} iff ex op, v being set st

( x = [op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st

( the Arity of S . op = args & n in dom args & args . n = v ) ) ) ) & ( for x being object holds

( x in b_{2} iff ex op, v being set st

( x = [op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st

( the Arity of S . op = args & n in dom args & args . n = v ) ) ) ) holds

b_{1} = b_{2}
; :: thesis: verum

( x in X1 iff S

( x in X2 iff S

X1 = X2 from XBOOLE_0:sch 3();

hence for b

( x in b

( x = [op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st

( the Arity of S . op = args & n in dom args & args . n = v ) ) ) ) & ( for x being object holds

( x in b

( x = [op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st

( the Arity of S . op = args & n in dom args & args . n = v ) ) ) ) holds

b