let f be FinSequence of REAL ; :: thesis: ( ( for y being Real st y in rng f holds
y >= 0 ) iff for i being Nat st i in dom f holds
f . i >= 0 )
hereby :: thesis: ( ( for i being Nat st i in dom f holds
f . i >= 0 ) implies for y being Real st y in rng f holds
y >= 0 )
assume A1: for y being Real st y in rng f holds
y >= 0 ; :: thesis: for i being Nat st i in dom f holds
f . i >= 0
hereby :: thesis: verum
let i be Nat; :: thesis: ( i in dom f implies f . i >= 0 )
assume i in dom f ; :: thesis: f . i >= 0
then f . i in rng f by FUNCT_1:def 3;
hence f . i >= 0 by A1; :: thesis: verum
end;
end;
assume A2: for i being Nat st i in dom f holds
f . i >= 0 ; :: thesis: for y being Real st y in rng f holds
y >= 0
hereby :: thesis: verum
let x be Real; :: thesis: ( x in rng f implies x >= 0 )
assume x in rng f ; :: thesis: x >= 0
then consider y being object such that
A3: y in dom f and
A4: x = f . y by FUNCT_1:def 3;
thus x >= 0 by A2, A3, A4; :: thesis: verum
end;