defpred S₁[ set ] 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 set 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

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:90;
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