let I be Program of ; :: thesis: UsedI*Loc I = UsedI*Loc (Directed I)
set A = { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng I } ;
set B = { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng (Directed I) } ;
A1: { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng I } c= { (UsedInt*Loc 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 { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng I } or e in { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng (Directed I) } )
assume e in { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng I } ; :: thesis: e in { (UsedInt*Loc 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 = UsedInt*Loc 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: UsedInt*Loc i = UsedInt*Loc j
end;
hence e in { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng (Directed I) } by A2, A6; :: thesis: verum
end;
{ (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng (Directed I) } c= { (UsedInt*Loc 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 { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng (Directed I) } or e in { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng I } )
assume e in { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng (Directed I) } ; :: thesis: e in { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng I }
then consider i being Instruction of SCM+FSA such that
A9: e = UsedInt*Loc i and
A10: i in rng (Directed I) ;
consider x being object such that
A11: x in dom (Directed I) and
A12: (Directed I) . x = i by A10, FUNCT_1:def 3;
set j = I . x;
A13: x in dom I by A11, FUNCT_4:99;
then A14: I . x in rng I by FUNCT_1:3;
reconsider j = I . x as Instruction of SCM+FSA by A14;
now :: thesis: UsedInt*Loc i = UsedInt*Loc j
end;
hence e in { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng I } by A9, A14; :: thesis: verum
end;
hence UsedI*Loc I = UsedI*Loc (Directed I) by A1, XBOOLE_0:def 10; :: thesis: verum