let a, b be Real; :: thesis: for n being Nat
for M1, M2 being Matrix of n,REAL st a >= 0 & b >= 0 & M1 is Nonnegative & M2 is Nonnegative holds
(a * M1) + (b * M2) is Nonnegative
let n be Nat; :: thesis: for M1, M2 being Matrix of n,REAL st a >= 0 & b >= 0 & M1 is Nonnegative & M2 is Nonnegative holds
(a * M1) + (b * M2) is Nonnegative
let M1, M2 be Matrix of n,REAL; :: thesis: ( a >= 0 & b >= 0 & M1 is Nonnegative & M2 is Nonnegative implies (a * M1) + (b * M2) is Nonnegative )
assume ( a >= 0 & b >= 0 & M1 is Nonnegative & M2 is Nonnegative ) ; :: thesis: (a * M1) + (b * M2) is Nonnegative
then ( a * M1 is Nonnegative & b * M2 is Nonnegative ) by Th42;
hence (a * M1) + (b * M2) is Nonnegative by Th36; :: thesis: verum