let D1, D2 be non empty set ; :: thesis: for M1 being Matrix of D1
for M2 being Matrix of D2 st M1 = M2 holds
for i being Nat st i in dom M1 holds
Line (M1,i) = Line (M2,i)
let M1 be Matrix of D1; :: thesis: for M2 being Matrix of D2 st M1 = M2 holds
for i being Nat st i in dom M1 holds
Line (M1,i) = Line (M2,i)
let M2 be Matrix of D2; :: thesis: ( M1 = M2 implies for i being Nat st i in dom M1 holds
Line (M1,i) = Line (M2,i) )
assume A1: M1 = M2 ; :: thesis: for i being Nat st i in dom M1 holds
Line (M1,i) = Line (M2,i)

hereby :: thesis: verum

let i be Nat; :: thesis: ( i in dom M1 implies Line (M1,i) = Line (M2,i) )
assume A2: i in dom M1 ; :: thesis: Line (M1,i) = Line (M2,i)
then Line (M1,i) = M1 . i by MATRIX_0:60;
hence Line (M1,i) = Line (M2,i) by A1, A2, MATRIX_0:60; :: thesis: verum

end;