defpred S₁[ Element of NAT ] means verum;
set S = { F₄(i) where i is Element of NAT : ( F₁() <= i & i <= F₂() & S₁[i] ) } ;
F₁() in NAT by ORDINAL1:def 13;
then A2: F₄(F₁()) in { F₄(i) where i is Element of NAT : ( F₁() <= i & i <= F₂() & S₁[i] ) } by A1;
set S1 = { F₄(i) where i is Element of NAT : ( F₁() <= i & i <= F₂() ) } ;

A3: now

let x be set ; :: thesis: ( ( x in { F₄(i) where i is Element of NAT : ( F₁() <= i & 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 Element of NAT : ( F₁() <= i & 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 Element of NAT : ( F₁() <= i & i <= F₂() & S₁[i] ) } )

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

end;

A4: { F₄(i) where i is Element of NAT : ( F₁() <= i & i <= F₂() & S₁[i] ) } c= F₃()

proof

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

end;

{ F₄(i) where i is Element of NAT : ( F₁() <= i & 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, A4, TARSKI:2; :: thesis: verum