deffunc H₁( Element of NAT ) -> Element of bool ExtREAL = In ([.-infty,(b - $1).],(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 = [.-infty,(b - n).]
let n be Nat; :: thesis: F . n = [.-infty,(b - n).]
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
A1: [.-infty,(b - nn).] c= ExtREAL by MEMBERED:2;
F . nn = H₁(nn) by A3
.= [.-infty,(b - nn).] by SUBSET_1:def 8, A1 ;
hence F . n = [.-infty,(b - n).] ; :: thesis: verum