A1: for z being FinSequence of REAL st ( for i being Element of NAT st i in dom z holds
z . i >= 0 ) holds
for i being Element of NAT holds z . i >= 0

proof

let z be FinSequence of REAL ; :: thesis: ( ( for i being Element of NAT st i in dom z holds
z . i >= 0 ) implies for i being Element of NAT holds z . i >= 0 )
assume A2: for i being Element of NAT st i in dom z holds
z . i >= 0 ; :: thesis: for i being Element of NAT holds z . i >= 0

hereby :: thesis: verum

let i be Element of NAT ; :: thesis: z . b₁ >= 0

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

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

hence z . i >= 0 by FUNCT_1:def 4; :: thesis: verum

end;

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

hence z . i >= 0 by A2; :: thesis: verum

end;

end;

end;

end;

let x, y be FinSequence of REAL ; :: thesis: ( ( for i being Element of NAT st i in dom x holds
x . i >= 0 ) & ( for i being Element of NAT st i in dom y holds
y . i >= 0 ) implies for k being Element of NAT st k in dom (mlt x,y) holds
(mlt x,y) . k >= 0 )
assume A3: ( ( for i being Element of NAT st i in dom x holds
x . i >= 0 ) & ( for i being Element of NAT st i in dom y holds
y . i >= 0 ) ) ; :: thesis: for k being Element of NAT st k in dom (mlt x,y) holds
(mlt x,y) . k >= 0

hereby :: thesis: verum

let k be Element of NAT ; :: thesis: ( k in dom (mlt x,y) implies (mlt x,y) . k >= 0 )
assume k in dom (mlt x,y) ; :: thesis: (mlt x,y) . k >= 0
then A4: (mlt x,y) . k = (x . k) * (y . k) by RVSUM_1:86;
( x . k >= 0 & y . k >= 0 ) by A3, A1;
hence (mlt x,y) . k >= 0 by A4, XREAL_1:129; :: thesis: verum

end;