set A = { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in X } ;

union { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in X } c= FinSeq-Locations

union { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in X } c= FinSeq-Locations

proof

hence
union { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in X } is Subset of FinSeq-Locations
; :: thesis: verum
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in union { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in X } or e in FinSeq-Locations )

assume e in union { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in X } ; :: thesis: e in FinSeq-Locations

then consider B being set such that

A1: e in B and

A2: B in { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in X } by TARSKI:def 4;

ex i being Instruction of SCM+FSA st

( B = UsedInt*Loc i & i in X ) by A2;

then B c= FinSeq-Locations by FINSUB_1:def 5;

hence e in FinSeq-Locations by A1; :: thesis: verum

end;assume e in union { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in X } ; :: thesis: e in FinSeq-Locations

then consider B being set such that

A1: e in B and

A2: B in { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in X } by TARSKI:def 4;

ex i being Instruction of SCM+FSA st

( B = UsedInt*Loc i & i in X ) by A2;

then B c= FinSeq-Locations by FINSUB_1:def 5;

hence e in FinSeq-Locations by A1; :: thesis: verum