defpred S₁[ object ] means ex f being Function of [:(C -States the generators of X), the carrier of A:],(C -States the generators of X) st
( $1 = f & f is ExecutionFunction of A,C -States the generators of X,z -States ( the generators of X,x) & ( for s being Element of C -States the generators of X
for b being SortSymbol of B
for v being Element of the generators of X . b
for v0 being Element of X,b st v0 = v holds
for t being Element of T,b holds f . (s,(v := (t,A))) = succ (s,v0,(t value_at (C,s))) ) );
consider Z being set such that
A1: for c being object holds
( c in Z iff ( c in Funcs ([:(C -States the generators of X), the carrier of A:],(C -States the generators of X)) & S₁[c] ) ) from XBOOLE_0:sch 1();
Z c= Funcs ([:(C -States the generators of X), the carrier of A:],(C -States the generators of X)) by A1;
then reconsider Z = Z as Subset of (Funcs ([:(C -States the generators of X), the carrier of A:],(C -States the generators of X))) ;
take Z ; :: thesis: for f being Function of [:(C -States the generators of X), the carrier of A:],(C -States the generators of X) holds
( f in Z iff ( f is ExecutionFunction of A,C -States the generators of X,z -States ( the generators of X,x) & ( for s being Element of C -States the generators of X
for b being SortSymbol of B
for v being Element of the generators of X . b
for v0 being Element of X,b st v0 = v holds
for t being Element of T,b holds f . (s,(v := (t,A))) = succ (s,v0,(t value_at (C,s))) ) ) )
let f be Function of [:(C -States the generators of X), the carrier of A:],(C -States the generators of X); :: thesis: ( f in Z iff ( f is ExecutionFunction of A,C -States the generators of X,z -States ( the generators of X,x) & ( for s being Element of C -States the generators of X
for b being SortSymbol of B
for v being Element of the generators of X . b
for v0 being Element of X,b st v0 = v holds
for t being Element of T,b holds f . (s,(v := (t,A))) = succ (s,v0,(t value_at (C,s))) ) ) )

hereby :: thesis: ( f is ExecutionFunction of A,C -States the generators of X,z -States ( the generators of X,x) & ( for s being Element of C -States the generators of X
for b being SortSymbol of B
for v being Element of the generators of X . b
for v0 being Element of X,b st v0 = v holds
for t being Element of T,b holds f . (s,(v := (t,A))) = succ (s,v0,(t value_at (C,s))) ) implies f in Z )

assume f in Z ; :: thesis: ( f is ExecutionFunction of A,C -States the generators of X,z -States ( the generators of X,x) & ( for s being Element of C -States the generators of X
for b being SortSymbol of B
for v being Element of the generators of X . b
for v0 being Element of X,b st v0 = v holds
for t being Element of T,b holds f . (s,(v := (t,A))) = succ (s,v0,(t value_at (C,s))) ) )
then S₁[f] by A1;
hence ( f is ExecutionFunction of A,C -States the generators of X,z -States ( the generators of X,x) & ( for s being Element of C -States the generators of X
for b being SortSymbol of B
for v being Element of the generators of X . b
for v0 being Element of X,b st v0 = v holds
for t being Element of T,b holds f . (s,(v := (t,A))) = succ (s,v0,(t value_at (C,s))) ) ) ; :: thesis: verum

end;

f in Funcs ([:(C -States the generators of X), the carrier of A:],(C -States the generators of X)) by FUNCT_2:8;
hence ( f is ExecutionFunction of A,C -States the generators of X,z -States ( the generators of X,x) & ( for s being Element of C -States the generators of X
for b being SortSymbol of B
for v being Element of the generators of X . b
for v0 being Element of X,b st v0 = v holds
for t being Element of T,b holds f . (s,(v := (t,A))) = succ (s,v0,(t value_at (C,s))) ) implies f in Z ) by A1; :: thesis: verum