let Z1, Z2 be Subset of (Funcs ([:(C -States the generators of X), the carrier of A:],(C -States the generators of X))); :: 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 Z1 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))) ) ) ) ) & ( for f being Function of [:(C -States the generators of X), the carrier of A:],(C -States the generators of X) holds
( f in Z2 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))) ) ) ) ) implies Z1 = Z2 )
assume that
A2: for f being Function of [:(C -States the generators of X), the carrier of A:],(C -States the generators of X) holds
( f in Z1 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))) ) ) ) and
A3: for f being Function of [:(C -States the generators of X), the carrier of A:],(C -States the generators of X) holds
( f in Z2 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))) ) ) ) ; :: thesis: Z1 = Z2
thus Z1 c= Z2 :: according to XBOOLE_0:def 10 :: thesis: Z2 c= Z1

proof

let c be object ; :: according to TARSKI:def 3 :: thesis: ( not c in Z1 or c in Z2 )
assume A4: c in Z1 ; :: thesis: c in Z2
then reconsider f = c as Function of [:(C -States the generators of X), the carrier of A:],(C -States the generators of X) by FUNCT_2:66;
( 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))) ) ) by A2, A4;
hence c in Z2 by A3; :: thesis: verum

end;

let c be object ; :: according to TARSKI:def 3 :: thesis: ( not c in Z2 or c in Z1 )
assume A5: c in Z2 ; :: thesis: c in Z1
then reconsider f = c as Function of [:(C -States the generators of X), the carrier of A:],(C -States the generators of X) by FUNCT_2:66;
( 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))) ) ) by A3, A5;
hence c in Z1 by A2; :: thesis: verum