let S1, S2 be SetSequence of ExtREAL; :: thesis: ( ( for n being Nat holds S1 . n = [.(b + n),+infty.] ) & ( for n being Nat holds S2 . n = [.(b + n),+infty.] ) implies S1 = S2 )

assume that

A4: for n being Nat holds S1 . n = [.(b + n),+infty.] and

A5: for n being Nat holds S2 . n = [.(b + n),+infty.] ; :: thesis: S1 = S2

for n being Element of NAT holds S1 . n = S2 . n

assume that

A4: for n being Nat holds S1 . n = [.(b + n),+infty.] and

A5: for n being Nat holds S2 . n = [.(b + n),+infty.] ; :: thesis: S1 = S2

for n being Element of NAT holds S1 . n = S2 . n

proof

hence
S1 = S2
; :: thesis: verum
let n be Element of NAT ; :: thesis: S1 . n = S2 . n

thus S1 . n = [.(b + n),+infty.] by A4

.= S2 . n by A5 ; :: thesis: verum

end;thus S1 . n = [.(b + n),+infty.] by A4

.= S2 . n by A5 ; :: thesis: verum