let A, B be Matrix of REAL; :: thesis: ( len A = len B & width A = width B implies for i being Nat st 1 <= i & i <= len A holds
Line ((A - B),i) = (Line (A,i)) - (Line (B,i)) )
assume that
A1: len A = len B and
A2: width A = width B ; :: thesis: for i being Nat st 1 <= i & i <= len A holds
Line ((A - B),i) = (Line (A,i)) - (Line (B,i))
A3: width (A - B) = width A by A1, A2, Th6;
let i be Nat; :: thesis: ( 1 <= i & i <= len A implies Line ((A - B),i) = (Line (A,i)) - (Line (B,i)) )
A4: len (Line (A,i)) = width A by MATRIX_0:def 7;
A5: len (Line (B,i)) = width B by MATRIX_0:def 7;
assume ( 1 <= i & i <= len A ) ; :: thesis: Line ((A - B),i) = (Line (A,i)) - (Line (B,i))
then A6: i in dom A by FINSEQ_3:25;
A7: for j being Nat st j in Seg (width (A - B)) holds
((Line (A,i)) - (Line (B,i))) . j = (A - B) * (i,j)

proof

reconsider i2 = i as Nat ;
let j be Nat; :: thesis: ( j in Seg (width (A - B)) implies ((Line (A,i)) - (Line (B,i))) . j = (A - B) * (i,j) )
reconsider j2 = j as Nat ;
A8: ((Line (A,i2)) - (Line (B,i2))) . j = ((Line (A,i2)) . j2) - ((Line (B,i2)) . j2) by A2, A4, A5, Lm1;
assume A9: j in Seg (width (A - B)) ; :: thesis: ((Line (A,i)) - (Line (B,i))) . j = (A - B) * (i,j)
then [i,j] in Indices A by A6, A3, ZFMISC_1:87;
then A10: (A - B) * (i2,j2) = (A * (i2,j2)) - (B * (i2,j2)) by A1, A2, Th6;
A11: j in Seg (width A) by A1, A2, A9, Th6;
then (Line (A,i)) . j = A * (i,j) by MATRIX_0:def 7;
hence ((Line (A,i)) - (Line (B,i))) . j = (A - B) * (i,j) by A2, A11, A10, A8, MATRIX_0:def 7; :: thesis: verum

end;

len ((Line (A,i)) - (Line (B,i))) = len (Line (A,i)) by A2, A4, A5, RVSUM_1:116;
hence Line ((A - B),i) = (Line (A,i)) - (Line (B,i)) by A4, A3, A7, MATRIX_0:def 7; :: thesis: verum