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 Element of 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 Element of 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 Element of NAT st i in dom M1 holds
Line M1,i = Line M2,i )
assume A1: M1 = M2 ; :: thesis: for i being Element of NAT st i in dom M1 holds
Line M1,i = Line M2,i

hereby :: thesis: verum

let i be Element of NAT ; :: thesis: ( i in dom M1 implies Line M1,i = Line M2,i )
assume i in dom M1 ; :: thesis: Line M1,i = Line M2,i
then ( Line M1,i = M1 . i & Line M2,i = M2 . i ) by A1, MATRIX_2:18;
hence Line M1,i = Line M2,i by A1; :: thesis: verum

end;