defpred S_{1}[ 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_{1}[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))) ) ) )

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

( $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

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 )

f in Funcs ([:(C -States the generators of X), the carrier of A:],(C -States the generators of X))
by FUNCT_2:8;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_{1}[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;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

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

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