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₁[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₁[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₁[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