theorem NDIFF823: :: LOPBAN11:10

for n being Nat
for F being Element of REAL n
for s being Real st ( for i being Nat st i in dom F holds
( 0 <= F . i & F . i <= s ) ) holds
|.F.| <= sqrt ((s * s) * (len F))