let I be Program of ; :: thesis: UsedILoc I = UsedILoc (Directed I)
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) }

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng I } or e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (Directed I) } )
assume e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng I } ; :: thesis: e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (Directed I) }
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;

now :: thesis: UsedIntLoc i = UsedIntLoc j

per cases ( i = halt SCM+FSA or i <> halt SCM+FSA ) ;

suppose A7: i = halt SCM+FSA ; :: thesis: UsedIntLoc i = UsedIntLoc j

then j = goto (card I) by A4, A5, FUNCT_4:106;
hence UsedIntLoc i = UsedIntLoc j by Th15, A7, Th13; :: thesis: verum

end;

suppose i <> halt SCM+FSA ; :: thesis: UsedIntLoc i = UsedIntLoc j

hence UsedIntLoc i = UsedIntLoc j by A5, FUNCT_4:105; :: thesis: verum

end;

end;

end;

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

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 }

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (Directed I) } or e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng I } )
assume e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (Directed I) } ; :: thesis: e in { (UsedIntLoc i) 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 (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;

now :: thesis: UsedIntLoc i = UsedIntLoc j

per cases ( j = halt SCM+FSA or j <> halt SCM+FSA ) ;

suppose A14: j = halt SCM+FSA ; :: thesis: UsedIntLoc i = UsedIntLoc j

then i = goto (card I) by A11, FUNCT_4:106, A12;
hence UsedIntLoc i = UsedIntLoc j by A14, Th13, Th15; :: thesis: verum

end;

suppose j <> halt SCM+FSA ; :: thesis: UsedIntLoc i = UsedIntLoc j

hence UsedIntLoc i = UsedIntLoc j by A11, FUNCT_4:105; :: thesis: verum

end;

end;

end;

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

end;

hence UsedILoc I = UsedILoc (Directed I) by A1, XBOOLE_0:def 10; :: thesis: verum