defpred S₁[ object ] means ex f being Function of VAR,E st
( $1 = (f * decode) | (code (Free H)) & f in St (H,E) );
consider B being set such that
A1: for p being object holds
( p in B iff ( p in Funcs ((code (Free H)),E) & S₁[p] ) ) from XBOOLE_0:sch 1();
take B ; :: thesis: for p being set holds
( p in B iff ex f being Function of VAR,E st
( p = (f * decode) | (code (Free H)) & f in St (H,E) ) )
for p being set holds
( p in B iff ex f being Function of VAR,E st
( p = (f * decode) | (code (Free H)) & f in St (H,E) ) )

proof

let p be set ; :: thesis: ( p in B iff ex f being Function of VAR,E st
( p = (f * decode) | (code (Free H)) & f in St (H,E) ) )

now :: thesis: ( ex f being Function of VAR,E st
( p = (f * decode) | (code (Free H)) & f in St (H,E) ) implies p in B )

given f being Function of VAR,E such that A2: p = (f * decode) | (code (Free H)) and
A3: f in St (H,E) ; :: thesis: p in B
dom (f * decode) = omega by FUNCT_2:def 1;
then dom ((f * decode) | (code (Free H))) = omega /\ (code (Free H)) by RELAT_1:61;
then A4: dom ((f * decode) | (code (Free H))) = code (Free H) by XBOOLE_1:28;
rng ((f * decode) | (code (Free H))) c= E ;
then p in Funcs ((code (Free H)),E) by A2, A4, FUNCT_2:def 2;
hence p in B by A1, A2, A3; :: thesis: verum

end;

hence ( p in B iff ex f being Function of VAR,E st
( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) by A1; :: thesis: verum

end;

hence for p being set holds
( p in B iff ex f being Function of VAR,E st
( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) ; :: thesis: verum