let I be Program of ; :: thesis:
set A = { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng I } ;
set B = { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (Directed I) } ;
A1: { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng I } c= { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (Directed I) }

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng I } ; :: thesis:
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 A3, FUNCT_1:def 3;
set j = (Directed I) . x;
x in dom (Directed I) by A4, FUNCT_4:99;
then A6: (Directed I) . x in rng (Directed I) by FUNCT_1:3;
reconsider j = (Directed I) . x as Instruction of SCM+FSA by A6;

end;

end;

hence e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (Directed I) } by A2, A6; :: thesis:

end;

{ (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (Directed I) } c= { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng I }

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (Directed I) } ; :: thesis:
then consider i being Instruction of SCM+FSA such that
A8: e = UsedIntLoc i and
A9: i in rng (Directed I) ;
consider x being object such that
A10: x in dom (Directed I) and
A11: (Directed I) . x = i by A9, FUNCT_1:def 3;
set j = I . x;
A12: x in dom I by A10, FUNCT_4:99;
then A13: I . x in rng I by FUNCT_1:3;
reconsider j = I . x as Instruction of SCM+FSA by A13;

end;

end;

hence e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng I } by A8, A13; :: thesis:

end;