for n being Nat
for M1, M2 being Matrix of n,REAL holds |:(M1 + M2):| is_less_or_equal_with |:M1:| + |:M2:|