let F be FinSequence of ExtREAL ; :: thesis: for G being ExtREAL_sequence st ( for i being Nat holds F . i = G . i ) holds
( F is nonnegative iff G is nonnegative )
let G be ExtREAL_sequence; :: thesis: ( ( for i being Nat holds F . i = G . i ) implies ( F is nonnegative iff G is nonnegative ) )
assume A1: for i being Nat holds F . i = G . i ; :: thesis: ( F is nonnegative iff G is nonnegative )

hereby :: thesis: ( G is nonnegative implies F is nonnegative )

assume A3: F is nonnegative ; :: thesis: G is nonnegative

now :: thesis: for i being object st i in dom G holds
G . i >= 0

let i be object ; :: thesis: ( i in dom G implies G . b₁ >= 0 )
assume A4: i in dom G ; :: thesis: G . b₁ >= 0

per cases ( i in dom F or not i in dom F ) ;

suppose i in dom F ; :: thesis: G . b₁ >= 0

then G . i = F . i by A1;
hence G . i >= 0 by A3, SUPINF_2:51; :: thesis: verum

end;

suppose not i in dom F ; :: thesis: G . b₁ >= 0

then F . i = 0 by FUNCT_1:def 2;
hence G . i >= 0 by A1, A4; :: thesis: verum

end;

end;

end;

hence G is nonnegative by SUPINF_2:52; :: thesis: verum

end;

assume A5: G is nonnegative ; :: thesis: F is nonnegative

now :: thesis: for i being object holds F . i >= 0

let i be object ; :: thesis: F . b₁ >= 0

per cases ( i in dom F or not i in dom F ) ;

suppose i in dom F ; :: thesis: F . b₁ >= 0

then F . i = G . i by A1;
hence F . i >= 0 by A5, SUPINF_2:51; :: thesis: verum

end;

suppose not i in dom F ; :: thesis: F . b₁ >= 0

hence F . i >= 0 by FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

hence F is nonnegative by SUPINF_2:51; :: thesis: verum