let D, E be non empty set ; for M being Matrix of D
for L being Matrix of E
for i being Nat st M = L & i in dom M holds
Line (M,i) = Line (L,i)
let M be Matrix of D; for L being Matrix of E
for i being Nat st M = L & i in dom M holds
Line (M,i) = Line (L,i)
let L be Matrix of E; for i being Nat st M = L & i in dom M holds
Line (M,i) = Line (L,i)
let i be Nat; ( M = L & i in dom M implies Line (M,i) = Line (L,i) )
assume AS1:
( M = L & i in dom M )
; Line (M,i) = Line (L,i)
A1:
( len (Line (M,i)) = width M & ( for j being Nat st j in Seg (width M) holds
(Line (M,i)) . j = M * (i,j) ) )
by MATRIX_0:def 7;
A2:
( len (Line (L,i)) = width L & ( for j being Nat st j in Seg (width L) holds
(Line (L,i)) . j = L * (i,j) ) )
by MATRIX_0:def 7;
A3: dom (Line (M,i)) =
Seg (width M)
by A1, FINSEQ_1:def 3
.=
dom (Line (L,i))
by AS1, A2, FINSEQ_1:def 3
;
for j being Nat st j in dom (Line (M,i)) holds
(Line (M,i)) . j = (Line (L,i)) . j
proof
let j be
Nat;
( j in dom (Line (M,i)) implies (Line (M,i)) . j = (Line (L,i)) . j )
assume
j in dom (Line (M,i))
;
(Line (M,i)) . j = (Line (L,i)) . j
then A4:
j in Seg (width M)
by FINSEQ_1:def 3, A1;
then
[i,j] in Indices M
by AS1, ZFMISC_1:87;
then A5:
M * (
i,
j)
= L * (
i,
j)
by AS1, EQ2;
thus (Line (M,i)) . j =
M * (
i,
j)
by A4, MATRIX_0:def 7
.=
(Line (L,i)) . j
by AS1, A4, A5, MATRIX_0:def 7
;
verum
end;
hence
Line (M,i) = Line (L,i)
by A3; verum