let I be Program of ; :: thesis:
set A = { () where i is Instruction of SCM+FSA : i in rng I } ;
set B = { () where i is Instruction of SCM+FSA : i in rng () } ;
A1: { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng I } c= { () where i is Instruction of SCM+FSA : i in rng () }
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { () where i is Instruction of SCM+FSA : i in rng I } or e in { () where i is Instruction of SCM+FSA : i in rng () } )
assume e in { () where i is Instruction of SCM+FSA : i in rng I } ; :: thesis: e in { () where i is Instruction of SCM+FSA : i in rng () }
then consider i being Instruction of SCM+FSA such that
A2: e = UsedIntLoc i and
A3: i in rng I ;
consider x being object such that
A4: x in dom I and
A5: I . x = i by ;
set j = () . x;
x in dom () by ;
then A6: (Directed I) . x in rng () by FUNCT_1:3;
reconsider j = () . x as Instruction of SCM+FSA by A6;
now :: thesis: end;
hence e in { () where i is Instruction of SCM+FSA : i in rng () } by A2, A6; :: thesis: verum
end;
{ (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng () } c= { () where i is Instruction of SCM+FSA : i in rng I }
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { () where i is Instruction of SCM+FSA : i in rng () } or e in { () where i is Instruction of SCM+FSA : i in rng I } )
assume e in { () where i is Instruction of SCM+FSA : i in rng () } ; :: thesis: e in { () where i is Instruction of SCM+FSA : i in rng I }
then consider i being Instruction of SCM+FSA such that
A8: e = UsedIntLoc i and
A9: i in rng () ;
consider x being object such that
A10: x in dom () and
A11: (Directed I) . x = i by ;
set j = I . x;
A12: x in dom I by ;
then A13: I . x in rng I by FUNCT_1:3;
reconsider j = I . x as Instruction of SCM+FSA by A13;
now :: thesis: end;
hence e in { () where i is Instruction of SCM+FSA : i in rng I } by ; :: thesis: verum
end;
hence UsedILoc I = UsedILoc () by ; :: thesis: verum