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