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

proof

let i be Nat; :: thesis: ( i in dom (Col (b,j)) implies (Col (b,j)) . i = (Col (B,j)) . i )
assume i in dom (Col (b,j)) ; :: thesis: (Col (b,j)) . i = (Col (B,j)) . i
then A5: i in dom b by A3, FINSEQ_1:def 3;
then [i,j] in [:(dom b),(Seg (width b)):] by A2, ZFMISC_1:87;
then A6: [i,j] in Indices b by MATRIX_0:def 4;
Indices b = [:(Seg n),(Seg n):] by MATRIX_0:24
.= Indices B by MATRIX_0:24 ;
then [i,j] in [:(dom B),(Seg (width B)):] by A6, MATRIX_0:def 4;
then A7: ( i in dom B & j in Seg (width B) ) by ZFMISC_1:87;
thus (Col (b,j)) . i = b * (i,j) by A5, MATRIX_0:def 8
.= B * (i,j) by A1, A6, Th83
.= (Col (B,j)) . i by A7, MATRIX_0:def 8 ; :: thesis: verum

end;

hence Col (b,j) = Col (B,j) by A1, A3, A4, FINSEQ_1:13; :: thesis: verum