let i be Nat; :: thesis: for K being Field
for A1, A2 being Matrix of K st width A1 = width A2 & i in dom A1 holds
Line ((A1 + A2),i) = (Line (A1,i)) + (Line (A2,i))
let K be Field; :: thesis: for A1, A2 being Matrix of K st width A1 = width A2 & i in dom A1 holds
Line ((A1 + A2),i) = (Line (A1,i)) + (Line (A2,i))
let A1, A2 be Matrix of K; :: thesis: ( width A1 = width A2 & i in dom A1 implies Line ((A1 + A2),i) = (Line (A1,i)) + (Line (A2,i)) )
assume that
A1: width A1 = width A2 and
A2: i in dom A1 ; :: thesis: Line ((A1 + A2),i) = (Line (A1,i)) + (Line (A2,i))
reconsider L1 = Line (A1,i), L2 = Line (A2,i) as Element of (width A1) -tuples_on the carrier of K by A1;