let D1, D2 be non empty set ; for M1 being Matrix of D1
for M2 being Matrix of D2 st M1 = M2 holds
for j being Nat st j in Seg (width M1) holds
Col (M1,j) = Col (M2,j)
let M1 be Matrix of D1; for M2 being Matrix of D2 st M1 = M2 holds
for j being Nat st j in Seg (width M1) holds
Col (M1,j) = Col (M2,j)
let M2 be Matrix of D2; ( M1 = M2 implies for j being Nat st j in Seg (width M1) holds
Col (M1,j) = Col (M2,j) )
assume A1:
M1 = M2
; for j being Nat st j in Seg (width M1) holds
Col (M1,j) = Col (M2,j)
hereby verum
let j be
Nat;
( j in Seg (width M1) implies Col (M1,j) = Col (M2,j) )assume A2:
j in Seg (width M1)
;
Col (M1,j) = Col (M2,j)A3:
for
k being
Nat st
k in dom (Col (M1,j)) holds
(Col (M1,j)) . k = (Col (M2,j)) . k
proof
let k be
Nat;
( k in dom (Col (M1,j)) implies (Col (M1,j)) . k = (Col (M2,j)) . k )
assume
k in dom (Col (M1,j))
;
(Col (M1,j)) . k = (Col (M2,j)) . k
then
k in Seg (len (Col (M1,j)))
by FINSEQ_1:def 3;
then A4:
k in Seg (len M1)
by MATRIX_0:def 8;
then A5:
[k,j] in Indices M1
by A2, Th12;
A6:
k in dom M1
by A4, FINSEQ_1:def 3;
hence (Col (M1,j)) . k =
M1 * (
k,
j)
by MATRIX_0:def 8
.=
M2 * (
k,
j)
by A1, A5, MATRIXR1:23
.=
(Col (M2,j)) . k
by A1, A6, MATRIX_0:def 8
;
verum
end; dom (Col (M1,j)) =
Seg (len (Col (M1,j)))
by FINSEQ_1:def 3
.=
Seg (len M1)
by MATRIX_0:def 8
.=
Seg (len (Col (M2,j)))
by A1, MATRIX_0:def 8
.=
dom (Col (M2,j))
by FINSEQ_1:def 3
;
hence
Col (
M1,
j)
= Col (
M2,
j)
by A3, FINSEQ_1:13;
verum
end;