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 V224() )
let G be ExtREAL_sequence; :: thesis: ( ( for i being Nat holds F . i = G . i ) implies ( F is nonnegative iff G is V224() ) )
assume A1: for i being Nat holds F . i = G . i ; :: thesis: ( F is nonnegative iff G is V224() )
hereby :: thesis: ( G is V224() implies F is nonnegative )
assume A3: F is nonnegative ; :: thesis: G is V224()
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 . b1 >= 0 )
assume A4: i in dom G ; :: thesis: G . b1 >= 0
per cases ( i in dom F or not i in dom F ) ;
suppose i in dom F ; :: thesis: G . b1 >= 0
then G . i = F . i by A1;
hence G . i >= 0 by A3, SUPINF_2:51; :: thesis: verum
end;
end;
end;
hence G is V224() by SUPINF_2:52; :: thesis: verum
end;
assume A5: G is V224() ; :: thesis: F is nonnegative
now :: thesis: for i being object holds F . i >= 0
let i be object ; :: thesis: F . b1 >= 0
per cases ( i in dom F or not i in dom F ) ;
suppose i in dom F ; :: thesis: F . b1 >= 0
then F . i = G . i by A1;
hence F . i >= 0 by A5, SUPINF_2:51; :: thesis: verum
end;
end;
end;
hence F is nonnegative by SUPINF_2:51; :: thesis: verum