defpred S₁[ Object of A] means for s being State of A
for a being Element of Values $1 holds Exec (I,s) = Exec (I,(s +* ($1,a)));
let a, b be Subset of A; :: thesis: ( ( for o being Object of A holds
( o in a iff for s being State of A
for a being Element of Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) ) ) & ( for o being Object of A holds
( o in b iff for s being State of A
for a being Element of Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) ) ) implies a = b )
assume that
A2: for o being Object of A holds
( o in a iff S₁[o] ) and
A3: for o being Object of A holds
( o in b iff S₁[o] ) ; :: thesis: a = b
thus a = b from SUBSET_1:sch 2(A2, A3); :: thesis: verum