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

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