let K be Field; for A, B being Matrix of K st width A = width B holds
for i being Nat st 1 <= i & i <= len A holds
Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
let A, B be Matrix of K; ( 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 A1:
width A = width B
; for i being Nat st 1 <= i & i <= len A holds
Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
let i be Nat; ( 1 <= i & i <= len A implies Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) )
assume
( 1 <= i & i <= len A )
; Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
then A2:
i in dom A
by FINSEQ_3:25;
reconsider LB = Line (B,i) as Element of (width A) -tuples_on the carrier of K by A1;