set S = { F₃(n) where n is Element of NAT : n <= F₁() } ;
set T = { F₃(n) where n is Element of NAT : ( 0 <= n & n <= F₁() ) } ;
A1: 0 <= F₁() ;
A2: { F₃(n) where n is Element of NAT : ( 0 <= n & n <= F₁() ) } is non empty finite Subset of F₂() from ASYMPT_0:sch 1(A1);

now

let x be set ; :: thesis: ( ( x in { F₃(n) where n is Element of NAT : n <= F₁() } implies x in { F₃(n) where n is Element of NAT : ( 0 <= n & n <= F₁() ) } ) & ( x in { F₃(n) where n is Element of NAT : ( 0 <= n & n <= F₁() ) } implies x in { F₃(n) where n is Element of NAT : n <= F₁() } ) )

hereby :: thesis: ( x in { F₃(n) where n is Element of NAT : ( 0 <= n & n <= F₁() ) } implies x in { F₃(n) where n is Element of NAT : n <= F₁() } )

assume x in { F₃(n) where n is Element of NAT : n <= F₁() } ; :: thesis: x in { F₃(n) where n is Element of NAT : ( 0 <= n & n <= F₁() ) }
then consider n being Element of NAT such that
A3: ( x = F₃(n) & n <= F₁() ) ;
thus x in { F₃(n) where n is Element of NAT : ( 0 <= n & n <= F₁() ) } by A3; :: thesis: verum

end;

assume x in { F₃(n) where n is Element of NAT : ( 0 <= n & n <= F₁() ) } ; :: thesis: x in { F₃(n) where n is Element of NAT : n <= F₁() }
then consider n being Element of NAT such that
A4: ( x = F₃(n) & 0 <= n & n <= F₁() ) ;
thus x in { F₃(n) where n is Element of NAT : n <= F₁() } by A4; :: thesis: verum

end;

hence { F₃(n) where n is Element of NAT : n <= F₁() } is non empty finite Subset of F₂() by A2, TARSKI:2; :: thesis: verum