defpred S_{1}[ set , set , set ] means for x, y being Subset of ExtREAL

for s being Nat st s = $1 & x = $2 & y = $3 holds

y = ].(b - (1 / (s + 1))),+infty.];

A1: for n being Nat

for x being Subset of ExtREAL ex y being Subset of ExtREAL st S_{1}[n,x,y]

consider F being SetSequence of ExtREAL such that

A2: F . 0 = AB and

A3: for n being Nat holds S_{1}[n,F . n,F . (n + 1)]
from RECDEF_1:sch 2(A1);

take F ; :: thesis: ( F . 0 = ].(b - 1),+infty.] & ( for n being Nat holds F . (n + 1) = ].(b - (1 / (n + 1))),+infty.] ) )

thus F . 0 = ].(b - 1),+infty.] by A2; :: thesis: for n being Nat holds F . (n + 1) = ].(b - (1 / (n + 1))),+infty.]

let n be Nat; :: thesis: F . (n + 1) = ].(b - (1 / (n + 1))),+infty.]

reconsider n = n as Element of NAT by ORDINAL1:def 12;

S_{1}[n,F . n,F . (n + 1)]
by A3;

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

for s being Nat st s = $1 & x = $2 & y = $3 holds

y = ].(b - (1 / (s + 1))),+infty.];

A1: for n being Nat

for x being Subset of ExtREAL ex y being Subset of ExtREAL st S

proof

reconsider AB = ].(b - 1),+infty.] as Subset of ExtREAL by MEMBERED:2;
let n be Nat; :: thesis: for x being Subset of ExtREAL ex y being Subset of ExtREAL st S_{1}[n,x,y]

let x be Subset of ExtREAL; :: thesis: ex y being Subset of ExtREAL st S_{1}[n,x,y]

reconsider AA = ].(b - (1 / (n + 1))),+infty.] as Subset of ExtREAL by MEMBERED:2;

take AA ; :: thesis: S_{1}[n,x,AA]

thus S_{1}[n,x,AA]
; :: thesis: verum

end;let x be Subset of ExtREAL; :: thesis: ex y being Subset of ExtREAL st S

reconsider AA = ].(b - (1 / (n + 1))),+infty.] as Subset of ExtREAL by MEMBERED:2;

take AA ; :: thesis: S

thus S

consider F being SetSequence of ExtREAL such that

A2: F . 0 = AB and

A3: for n being Nat holds S

take F ; :: thesis: ( F . 0 = ].(b - 1),+infty.] & ( for n being Nat holds F . (n + 1) = ].(b - (1 / (n + 1))),+infty.] ) )

thus F . 0 = ].(b - 1),+infty.] by A2; :: thesis: for n being Nat holds F . (n + 1) = ].(b - (1 / (n + 1))),+infty.]

let n be Nat; :: thesis: F . (n + 1) = ].(b - (1 / (n + 1))),+infty.]

reconsider n = n as Element of NAT by ORDINAL1:def 12;

S

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