set XX = [: the carrier' of S, the carrier of S:];

consider X being set such that

A1: for x being object holds

( x in X iff ( x in [: the carrier' of S, the carrier of S:] & S_{1}[x] ) )
from XBOOLE_0:sch 1();

take X ; :: thesis: for x being object holds

( x in X 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 ) ) )

let x be object ; :: thesis: ( x in X 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 ) ) )

thus ( x in X implies S_{1}[x] )
by A1; :: thesis: ( 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 ) ) implies x in X )

assume A2: S_{1}[x]
; :: thesis: x in X

then x in [: the carrier' of S, the carrier of S:] by ZFMISC_1:def 2;

hence x in X by A1, A2; :: thesis: verum

consider X being set such that

A1: for x being object holds

( x in X iff ( x in [: the carrier' of S, the carrier of S:] & S

take X ; :: thesis: for x being object holds

( x in X 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 ) ) )

let x be object ; :: thesis: ( x in X 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 ) ) )

thus ( x in X implies S

( 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 ) ) implies x in X )

assume A2: S

then x in [: the carrier' of S, the carrier of S:] by ZFMISC_1:def 2;

hence x in X by A1, A2; :: thesis: verum