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

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

( 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 Z2 or c in Z1 )
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;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

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