deffunc H₁( Element of NAT ) -> Element of bool ExtREAL = In ([.(b + $1),+infty.],(bool ExtREAL));
consider F being SetSequence of ExtREAL such that
A3: for n being Element of NAT holds F . n = H₁(n) from FUNCT_2:sch 4();
take F ; :: thesis: for n being Nat holds F . n = [.(b + n),+infty.]
let n be Nat; :: thesis: F . n = [.(b + n),+infty.]
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
A1: [.(b + nn),+infty.] c= ExtREAL by MEMBERED:2;
F . nn = H₁(nn) by A3
.= [.(b + nn),+infty.] by SUBSET_1:def 8, A1 ;
hence F . n = [.(b + n),+infty.] ; :: thesis: verum