defpred S₁[ set ] means ex e being Element of E st
( e in E & $1 = <%e%> );
consider C being Subset of (E ^omega) such that
A1: for x being set holds
( x in C iff ( x in E ^omega & S₁[x] ) ) from SUBSET_1:sch 1();
take C ; :: thesis: for x being set holds
( x in C iff ex e being Element of E st
( e in E & x = <%e%> ) )
for x being set holds
( x in C iff ex e being Element of E st
( e in E & x = <%e%> ) )

proof

let x be set ; :: thesis: ( x in C iff ex e being Element of E st
( e in E & x = <%e%> ) )
thus ( x in C implies ex e being Element of E st
( e in E & x = <%e%> ) ) by A1; :: thesis: ( ex e being Element of E st
( e in E & x = <%e%> ) implies x in C )
given e being Element of E such that A2: e in E and
A3: x = <%e%> ; :: thesis: x in C
{e} c= E by A2, ZFMISC_1:31;
then rng <%e%> c= E by AFINSQ_1:33;
then <%e%> is XFinSequence of E by RELAT_1:def 19;
then <%e%> is Element of E ^omega by AFINSQ_1:def 7;
hence x in C by A1, A2, A3; :: thesis: verum

end;

hence for x being set holds
( x in C iff ex e being Element of E st
( e in E & x = <%e%> ) ) ; :: thesis: verum