defpred S₁[ Nat] means F₁() <= $1;
set S = { F₄(i) where i is Nat : ( i <= F₂() & S₁[i] ) } ;
A2: F₄(F₁()) in { F₄(i) where i is Nat : ( i <= F₂() & S₁[i] ) } by A1;
set S1 = { F₄(i) where i is Element of NAT : ( F₁() <= i & i <= F₂() ) } ;

A3: now :: thesis: for x being object holds
( ( x in { F₄(i) where i is Nat : ( i <= F₂() & S₁[i] ) } implies x in { F₄(i) where i is Element of NAT : ( F₁() <= i & i <= F₂() ) } ) & ( x in { F₄(i) where i is Element of NAT : ( F₁() <= i & i <= F₂() ) } implies x in { F₄(i) where i is Nat : ( i <= F₂() & S₁[i] ) } ) )

let x be object ; :: thesis: ( ( x in { F₄(i) where i is Nat : ( i <= F₂() & S₁[i] ) } implies x in { F₄(i) where i is Element of NAT : ( F₁() <= i & i <= F₂() ) } ) & ( x in { F₄(i) where i is Element of NAT : ( F₁() <= i & i <= F₂() ) } implies x in { F₄(i) where i is Nat : ( i <= F₂() & S₁[i] ) } ) )

hereby :: thesis: ( x in { F₄(i) where i is Element of NAT : ( F₁() <= i & i <= F₂() ) } implies x in { F₄(i) where i is Nat : ( i <= F₂() & S₁[i] ) } )

assume x in { F₄(i) where i is Nat : ( i <= F₂() & S₁[i] ) } ; :: thesis: x in { F₄(i) where i is Element of NAT : ( F₁() <= i & i <= F₂() ) }
then consider i being Nat such that
A4: ( x = F₄(i) & i <= F₂() & S₁[i] ) ;
reconsider j = i as Element of NAT by ORDINAL1:def 12;
x = F₄(j) by A4;
hence x in { F₄(i) where i is Element of NAT : ( F₁() <= i & i <= F₂() ) } by A4; :: thesis: verum

end;

assume x in { F₄(i) where i is Element of NAT : ( F₁() <= i & i <= F₂() ) } ; :: thesis: x in { F₄(i) where i is Nat : ( i <= F₂() & S₁[i] ) }
then ex i being Element of NAT st
( x = F₄(i) & F₁() <= i & i <= F₂() ) ;
hence x in { F₄(i) where i is Nat : ( i <= F₂() & S₁[i] ) } ; :: thesis: verum

end;

A5: { F₄(i) where i is Nat : ( i <= F₂() & S₁[i] ) } c= F₃()

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₄(i) where i is Nat : ( i <= F₂() & S₁[i] ) } or x in F₃() )
assume x in { F₄(i) where i is Nat : ( i <= F₂() & S₁[i] ) } ; :: thesis: x in F₃()
then ex n1 being Nat st
( x = F₄(n1) & n1 <= F₂() & n1 >= F₁() ) ;
hence x in F₃() ; :: thesis: verum

end;

{ F₄(i) where i is Nat : ( i <= F₂() & S₁[i] ) } is finite from FINSEQ_1:sch 6();
hence { F₄(i) where i is Element of NAT : ( F₁() <= i & i <= F₂() ) } is non empty finite Subset of F₃() by A3, A2, A5, TARSKI:2; :: thesis: verum