let R be Ring; :: thesis: for n being Nat
for S being Subring of R
for a being Matrix of n,S
for A being Matrix of n,R st a = A holds
for i being Nat st i in dom a holds
Line (a,i) = Line (A,i)
let n be Nat; :: thesis: for S being Subring of R
for a being Matrix of n,S
for A being Matrix of n,R st a = A holds
for i being Nat st i in dom a holds
Line (a,i) = Line (A,i)
let S be Subring of R; :: thesis: for a being Matrix of n,S
for A being Matrix of n,R st a = A holds
for i being Nat st i in dom a holds
Line (a,i) = Line (A,i)
let a be Matrix of n,S; :: thesis: for A being Matrix of n,R st a = A holds
for i being Nat st i in dom a holds
Line (a,i) = Line (A,i)
let A be Matrix of n,R; :: thesis: ( a = A implies for i being Nat st i in dom a holds
Line (a,i) = Line (A,i) )
assume A1: a = A ; :: thesis: for i being Nat st i in dom a holds
Line (a,i) = Line (A,i)
let i be Nat; :: thesis: ( i in dom a implies Line (a,i) = Line (A,i) )
assume A2: i in dom a ; :: thesis: Line (a,i) = Line (A,i)
A3: dom (Line (a,i)) = Seg (len (Line (a,i))) by FINSEQ_1:def 3
.= Seg (width a) by MATRIX_0:def 7 ;
A4: Seg (width A) = Seg (len (Line (A,i))) by MATRIX_0:def 7
.= dom (Line (A,i)) by FINSEQ_1:def 3 ;
for j being Nat st j in dom (Line (a,i)) holds
(Line (a,i)) . j = (Line (A,i)) . j

proof

let j be Nat; :: thesis: ( j in dom (Line (a,i)) implies (Line (a,i)) . j = (Line (A,i)) . j )
assume A5: j in dom (Line (a,i)) ; :: thesis: (Line (a,i)) . j = (Line (A,i)) . j
then [i,j] in [:(dom a),(Seg (width a)):] by A2, A3, ZFMISC_1:87;
then A6: [i,j] in Indices a by MATRIX_0:def 4;
thus (Line (a,i)) . j = a * (i,j) by A3, A5, MATRIX_0:def 7
.= A * (i,j) by A1, A6, Th83
.= (Line (A,i)) . j by A1, A3, A5, MATRIX_0:def 7 ; :: thesis: verum

end;

hence Line (a,i) = Line (A,i) by A1, A3, A4, FINSEQ_1:13; :: thesis: verum