defpred S₁[ set , set ] means ex I being Instruction of SCM+FSA st
( $1 = I & $2 = UsedInt*Loc I );
A1: for e being Element of the Instructions of SCM+FSA ex u being Element of Fin FinSeq-Locations st S₁[e,u]

proof

let e be Element of the Instructions of SCM+FSA; :: thesis: ex u being Element of Fin FinSeq-Locations st S₁[e,u]
reconsider f = e as Instruction of SCM+FSA ;
reconsider u = UsedInt*Loc f as Element of Fin FinSeq-Locations ;
take u ; :: thesis: S₁[e,u]
take f ; :: thesis: ( e = f & u = UsedInt*Loc f )
thus ( e = f & u = UsedInt*Loc f ) ; :: thesis: verum

end;

consider UIL being Function of the Instructions of SCM+FSA,(Fin FinSeq-Locations) such that
A2: for i being Element of the Instructions of SCM+FSA holds S₁[i,UIL . i] from FUNCT_2:sch 3(A1);
set IT = Union (UIL * p);
set Up = UIL * p;
take Union (UIL * p) ; :: thesis: ( Union (UIL * p) is Subset of FinSeq-Locations & ex UIL being Function of the Instructions of SCM+FSA,(Fin FinSeq-Locations) st
( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & Union (UIL * p) = Union (UIL * p) ) )
Fin FinSeq-Locations c= bool FinSeq-Locations by FINSUB_1:26;
then ( rng (UIL * p) c= rng UIL & rng UIL c= bool FinSeq-Locations ) by RELAT_1:45, XBOOLE_1:1;
then rng (UIL * p) c= bool FinSeq-Locations by XBOOLE_1:1;
then ( Union (UIL * p) = union (rng (UIL * p)) & union (rng (UIL * p)) c= union (bool FinSeq-Locations) ) by CARD_3:def 4, ZFMISC_1:95;
hence Union (UIL * p) is Subset of FinSeq-Locations by ZFMISC_1:99; :: thesis: ex UIL being Function of the Instructions of SCM+FSA,(Fin FinSeq-Locations) st
( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & Union (UIL * p) = Union (UIL * p) )
take UIL ; :: thesis: ( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & Union (UIL * p) = Union (UIL * p) )

hereby :: thesis: Union (UIL * p) = Union (UIL * p)

let i be Instruction of SCM+FSA; :: thesis: UIL . i = UsedInt*Loc i
S₁[i,UIL . i] by A2;
hence UIL . i = UsedInt*Loc i ; :: thesis: verum

end;

thus Union (UIL * p) = Union (UIL * p) ; :: thesis: verum