deffunc H_{1}( 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_{1}(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_{1}(nn)
by A3

.= [.-infty,(b - nn).] by SUBSET_1:def 8, A1 ;

hence F . n = [.-infty,(b - n).] ; :: thesis: verum

consider F being SetSequence of ExtREAL such that

A3: for n being Element of NAT holds F . n = H

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

.= [.-infty,(b - nn).] by SUBSET_1:def 8, A1 ;

hence F . n = [.-infty,(b - n).] ; :: thesis: verum