for b₁ being Field
for b₂ being Matrix of b₁ st len b₂ > 0 holds
- (- b₂) = b₂

for b₁ being Field
for b₂ being Matrix of b₁ st len b₂ > 0 holds
b₂ + (- b₂) = 0. b₁,(len b₂),(width b₂)

for b₁ being Field
for b₂ being Matrix of b₁ st len b₂ > 0 holds
b₂ - b₂ = 0. b₁,(len b₂),(width b₂) by Th2;

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & width b₂ = width b₃ & width b₃ = width b₄ & len b₂ > 0 & b₂ + b₄ = b₃ + b₄ holds
b₂ = b₃

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st len b₃ > 0 holds
b₂ - (- b₃) = b₂ + b₃ by Th1;

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st len b₂ = len b₃ & width b₂ = width b₃ & len b₂ > 0 & b₂ = b₂ + b₃ holds
b₃ = 0. b₁,(len b₂),(width b₂)

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st len b₂ = len b₃ & width b₂ = width b₃ & len b₂ > 0 & b₂ - b₃ = 0. b₁,(len b₂),(width b₂) holds
b₂ = b₃

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st len b₂ = len b₃ & width b₂ = width b₃ & len b₂ > 0 & b₂ + b₃ = 0. b₁,(len b₂),(width b₂) holds
b₃ = - b₂

for b₁, b₂ being Nat
for b₃ being Field st b₁ > 0 holds
- (0. b₃,b₁,b₂) = 0. b₃,b₁,b₂

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st len b₂ = len b₃ & width b₂ = width b₃ & len b₂ > 0 & b₃ - b₂ = b₃ holds
b₂ = 0. b₁,(len b₂),(width b₂)

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st len b₂ = len b₃ & width b₂ = width b₃ & len b₂ > 0 holds
b₂ = b₂ - (b₃ - b₃)

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st len b₂ = len b₃ & width b₂ = width b₃ & len b₂ > 0 holds
- (b₂ + b₃) = (- b₂) + (- b₃)

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st len b₂ = len b₃ & width b₂ = width b₃ & len b₂ > 0 holds
b₂ - (b₂ - b₃) = b₃

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & width b₂ = width b₃ & width b₃ = width b₄ & len b₂ > 0 & b₂ - b₄ = b₃ - b₄ holds
b₂ = b₃

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & width b₂ = width b₃ & width b₃ = width b₄ & len b₂ > 0 & b₄ - b₂ = b₄ - b₃ holds
b₂ = b₃

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & width b₂ = width b₃ & width b₃ = width b₄ & len b₂ > 0 holds
(b₂ - b₃) - b₄ = (b₂ - b₄) - b₃

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & width b₂ = width b₃ & width b₃ = width b₄ & len b₂ > 0 holds
b₂ - b₄ = (b₂ - b₃) - (b₄ - b₃)

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & width b₂ = width b₃ & width b₃ = width b₄ & len b₂ > 0 holds
(b₄ - b₂) - (b₄ - b₃) = b₃ - b₂

for b₁ being Field
for b₂, b₃, b₄, b₅ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & len b₄ = len b₅ & width b₂ = width b₃ & width b₃ = width b₄ & width b₄ = width b₅ & len b₂ > 0 & b₂ - b₃ = b₄ - b₅ holds
b₂ - b₄ = b₃ - b₅

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st len b₂ = len b₃ & width b₂ = width b₃ & len b₂ > 0 holds
b₂ = b₂ + (b₃ - b₃)

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st len b₂ = len b₃ & width b₂ = width b₃ & len b₂ > 0 holds
b₂ = (b₂ + b₃) - b₃

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st len b₂ = len b₃ & width b₂ = width b₃ & len b₂ > 0 holds
b₂ = (b₂ - b₃) + b₃

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & width b₂ = width b₃ & width b₃ = width b₄ & len b₂ > 0 holds
b₂ + b₄ = (b₂ + b₃) + (b₄ - b₃)

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & width b₂ = width b₃ & width b₃ = width b₄ & len b₂ > 0 holds
(b₂ + b₃) - b₄ = (b₂ - b₄) + b₃

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & width b₂ = width b₃ & width b₃ = width b₄ & len b₂ > 0 holds
(b₂ - b₃) + b₄ = (b₄ - b₃) + b₂

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & width b₂ = width b₃ & width b₃ = width b₄ & len b₂ > 0 holds
b₂ + b₄ = (b₂ + b₃) - (b₃ - b₄)

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & width b₂ = width b₃ & width b₃ = width b₄ & len b₂ > 0 holds
b₂ - b₄ = (b₂ + b₃) - (b₄ + b₃)

for b₁ being Field
for b₂, b₃, b₄, b₅ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & len b₄ = len b₅ & width b₂ = width b₃ & width b₃ = width b₄ & width b₄ = width b₅ & len b₂ > 0 & b₂ + b₃ = b₄ + b₅ holds
b₂ - b₄ = b₅ - b₃

for b₁ being Field
for b₂, b₃, b₄, b₅ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & len b₄ = len b₅ & width b₂ = width b₃ & width b₃ = width b₄ & width b₄ = width b₅ & len b₂ > 0 & b₂ - b₄ = b₅ - b₃ holds
b₂ + b₃ = b₄ + b₅

for b₁ being Field
for b₂, b₃, b₄, b₅ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & len b₄ = len b₅ & width b₂ = width b₃ & width b₃ = width b₄ & width b₄ = width b₅ & len b₂ > 0 & b₂ + b₃ = b₄ - b₅ holds
b₂ + b₅ = b₄ - b₃

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & width b₂ = width b₃ & width b₃ = width b₄ & len b₂ > 0 holds
b₂ - (b₃ + b₄) = (b₂ - b₃) - b₄

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & width b₂ = width b₃ & width b₃ = width b₄ & len b₂ > 0 holds
b₂ - (b₃ - b₄) = (b₂ - b₃) + b₄

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & width b₂ = width b₃ & width b₃ = width b₄ & len b₂ > 0 holds
b₂ - (b₃ - b₄) = b₂ + (b₄ - b₃)

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & width b₂ = width b₃ & width b₃ = width b₄ & len b₂ > 0 holds
b₂ - b₄ = (b₂ - b₃) + (b₃ - b₄)

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & width b₂ = width b₃ & width b₃ = width b₄ & len b₂ > 0 & - b₂ = - b₃ holds
b₂ = b₃

for b₁ being Field
for b₂ being Matrix of b₁ st len b₂ > 0 & - b₂ = 0. b₁,(len b₂),(width b₂) holds
b₂ = 0. b₁,(len b₂),(width b₂)

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st len b₂ = len b₃ & width b₂ = width b₃ & len b₂ > 0 & b₂ + (- b₃) = 0. b₁,(len b₂),(width b₂) holds
b₂ = b₃

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st len b₂ = len b₃ & width b₂ = width b₃ & len b₂ > 0 holds
b₂ = (b₂ + b₃) + (- b₃)

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st len b₂ = len b₃ & width b₂ = width b₃ & len b₂ > 0 holds
b₂ = b₂ + (b₃ + (- b₃))

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st len b₂ = len b₃ & width b₂ = width b₃ & len b₂ > 0 holds
b₂ = ((- b₃) + b₂) + b₃

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st len b₂ = len b₃ & width b₂ = width b₃ & len b₂ > 0 holds
- ((- b₂) + b₃) = b₂ + (- b₃)

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st len b₂ = len b₃ & width b₂ = width b₃ & len b₂ > 0 holds
b₂ + b₃ = - ((- b₂) + (- b₃))

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st len b₂ = len b₃ & width b₂ = width b₃ & len b₂ > 0 holds
- (b₂ - b₃) = b₃ - b₂

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st len b₂ = len b₃ & width b₂ = width b₃ & len b₂ > 0 holds
(- b₂) - b₃ = (- b₃) - b₂

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st len b₂ = len b₃ & width b₂ = width b₃ & len b₂ > 0 holds
b₂ = (- b₃) - ((- b₂) - b₃)

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & width b₂ = width b₃ & width b₃ = width b₄ & len b₂ > 0 holds
((- b₂) - b₃) - b₄ = ((- b₂) - b₄) - b₃

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & width b₂ = width b₃ & width b₃ = width b₄ & len b₂ > 0 holds
((- b₂) - b₃) - b₄ = ((- b₃) - b₄) - b₂

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & width b₂ = width b₃ & width b₃ = width b₄ & len b₂ > 0 holds
((- b₂) - b₃) - b₄ = ((- b₄) - b₃) - b₂

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & width b₂ = width b₃ & width b₃ = width b₄ & len b₂ > 0 holds
(b₄ - b₂) - (b₄ - b₃) = - (b₂ - b₃)

for b₁ being Field
for b₂ being Matrix of b₁ st len b₂ > 0 holds
(0. b₁,(len b₂),(width b₂)) - b₂ = - b₂

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st len b₂ = len b₃ & width b₂ = width b₃ & len b₂ > 0 holds
b₂ + b₃ = b₂ - (- b₃) by Th5;

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st len b₂ = len b₃ & width b₂ = width b₃ & len b₂ > 0 holds
b₂ = b₂ - (b₃ + (- b₃))

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & width b₂ = width b₃ & width b₃ = width b₄ & len b₂ > 0 & b₂ - b₄ = b₃ + (- b₄) holds
b₂ = b₃

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₂ = len b₃ & len b₃ = len b₄ & width b₂ = width b₃ & width b₃ = width b₄ & len b₂ > 0 & b₄ - b₂ = b₄ + (- b₃) holds
b₂ = b₃

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st len b₂ = len b₃ & width b₂ = width b₃ holds
Indices b₂ = Indices b₃

for b₁ being Field
for b₂, b₃, b₄ being FinSequence of b₁ st len b₂ = len b₃ & len b₃ = len b₄ holds
mlt (b₂ + b₃),b₄ = (mlt b₂,b₄) + (mlt b₃,b₄)

for b₁ being Field
for b₂, b₃, b₄ being FinSequence of b₁ st len b₂ = len b₃ & len b₃ = len b₄ holds
mlt b₄,(b₂ + b₃) = (mlt b₄,b₂) + (mlt b₄,b₃)

for b₁ being non empty set
for b₂ being Matrix of b₁ st len b₂ > 0 holds
for b₃ being Nat holds
( b₂ is Matrix of b₃, width b₂,b₁ iff b₃ = len b₂ ) by MATRIX_1:20, MATRIX_1:def 3;

for b₁ being Nat
for b₂ being Field
for b₃ being Nat
for b₄, b₅ being Matrix of b₂ st len b₄ = len b₅ & width b₄ = width b₅ & ex b₆ being Nat st [b₁,b₆] in Indices b₄ holds
Line (b₄ + b₅),b₁ = (Line b₄,b₁) + (Line b₅,b₁)

for b₁ being Field
for b₂ being Nat
for b₃, b₄ being Matrix of b₁ st len b₃ = len b₄ & width b₃ = width b₄ & ex b₅ being Nat st [b₅,b₂] in Indices b₃ holds
Col (b₃ + b₄),b₂ = (Col b₃,b₂) + (Col b₄,b₂)

for b₁ being Field
for b₂, b₃ being FinSequence of b₁ st len b₂ = len b₃ holds
Sum (b₂ + b₃) = (Sum b₂) + (Sum b₃)

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₃ = len b₄ & width b₃ = width b₄ & width b₂ = len b₃ & len b₂ > 0 & len b₃ > 0 holds
b₂ * (b₃ + b₄) = (b₂ * b₃) + (b₂ * b₄)

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₃ = len b₄ & width b₃ = width b₄ & len b₂ = width b₃ & len b₃ > 0 & len b₂ > 0 holds
(b₃ + b₄) * b₂ = (b₃ * b₂) + (b₄ * b₂)

for b₁ being Field
for b₂, b₃, b₄ being Nat
for b₅ being Matrix of b₂,b₃,b₁
for b₆ being Matrix of b₃,b₄,b₁ st width b₅ = len b₆ & 0 < len b₅ & 0 < len b₆ holds
b₅ * b₆ is Matrix of b₂,b₄,b₁