set M = { F₅(w) where w is Instruction-Location of F₃() : w in F₄() } ;
consider f being Function such that
A2: dom f = F₄() /\ F₁() and
A3: for y being set st y in F₄() /\ F₁() holds
f . y = F₅(y) from FUNCT_1:sch 3();
{ F₅(w) where w is Instruction-Location of F₃() : w in F₄() } = f .: F₄()

proof

thus { F₅(w) where w is Instruction-Location of F₃() : w in F₄() } c= f .: F₄() :: according to XBOOLE_0:def 10 :: thesis: f .: F₄() c= { F₅(w) where w is Instruction-Location of F₃() : w in F₄() }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₅(w) where w is Instruction-Location of F₃() : w in F₄() } or x in f .: F₄() )
assume x in { F₅(w) where w is Instruction-Location of F₃() : w in F₄() } ; :: thesis: x in f .: F₄()
then consider u being Instruction-Location of F₃() such that
A4: x = F₅(u) and
A5: u in F₄() ;
u in F₁() by Def4;
then A6: u in dom f by A2, A5, XBOOLE_0:def 4;
then f . u = F₅(u) by A2, A3;
hence x in f .: F₄() by A4, A5, A6, FUNCT_1:def 12; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in f .: F₄() or x in { F₅(w) where w is Instruction-Location of F₃() : w in F₄() } )
assume x in f .: F₄() ; :: thesis: x in { F₅(w) where w is Instruction-Location of F₃() : w in F₄() }
then consider y being set such that
A7: y in dom f and
A8: y in F₄() and
A9: x = f . y by FUNCT_1:def 12;
y is Element of F₁() by A2, A7, XBOOLE_0:def 4;
then reconsider y = y as Instruction-Location of F₃() by Def4;
x = F₅(y) by A2, A3, A7, A9;
hence x in { F₅(w) where w is Instruction-Location of F₃() : w in F₄() } by A8; :: thesis: verum

end;

hence { F₅(w) where w is Instruction-Location of F₃() : w in F₄() } is finite by A1; :: thesis: verum