defpred S1[ 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 S1[n,x,y]
proof
let n be Nat; :: thesis: for x being Subset of ExtREAL ex y being Subset of ExtREAL st S1[n,x,y]
let x be Subset of ExtREAL; :: thesis: ex y being Subset of ExtREAL st S1[n,x,y]
reconsider AA = ].(b - (1 / (n + 1))),+infty.] as Subset of ExtREAL by MEMBERED:2;
take AA ; :: thesis: S1[n,x,AA]
thus S1[n,x,AA] ; :: thesis: verum
end;
reconsider AB = ].(b - 1),+infty.] as Subset of ExtREAL by MEMBERED:2;
consider F being SetSequence of ExtREAL such that
A2: F . 0 = AB and
A3: for n being Nat holds S1[n,F . n,F . (n + 1)] from 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;
S1[n,F . n,F . (n + 1)] by A3;
hence F . (n + 1) = ].(b - (1 / (n + 1))),+infty.] ; :: thesis: verum