let n, m, c be Nat; :: thesis: for D being non empty set
for AD being Matrix of n,m,D
for pD being FinSequence of D
for i being Nat st i in Seg (width AD) holds
( ( i = c & len pD = len AD implies Col (RCol AD,c,pD),i = pD ) & ( i <> c implies Col (RCol AD,c,pD),i = Col AD,i ) )
let D be non empty set ; :: thesis: for AD being Matrix of n,m,D
for pD being FinSequence of D
for i being Nat st i in Seg (width AD) holds
( ( i = c & len pD = len AD implies Col (RCol AD,c,pD),i = pD ) & ( i <> c implies Col (RCol AD,c,pD),i = Col AD,i ) )
let AD be Matrix of n,m,D; :: thesis: for pD being FinSequence of D
for i being Nat st i in Seg (width AD) holds
( ( i = c & len pD = len AD implies Col (RCol AD,c,pD),i = pD ) & ( i <> c implies Col (RCol AD,c,pD),i = Col AD,i ) )
let pD be FinSequence of D; :: thesis: for i being Nat st i in Seg (width AD) holds
( ( i = c & len pD = len AD implies Col (RCol AD,c,pD),i = pD ) & ( i <> c implies Col (RCol AD,c,pD),i = Col AD,i ) )
let i be Nat; :: thesis: ( i in Seg (width AD) implies ( ( i = c & len pD = len AD implies Col (RCol AD,c,pD),i = pD ) & ( i <> c implies Col (RCol AD,c,pD),i = Col AD,i ) ) )
assume A1: i in Seg (width AD) ; :: thesis: ( ( i = c & len pD = len AD implies Col (RCol AD,c,pD),i = pD ) & ( i <> c implies Col (RCol AD,c,pD),i = Col AD,i ) )
set R = RCol AD,c,pD;
set CR = Col (RCol AD,c,pD),i;
set CA = Col AD,i;
thus ( i = c & len pD = len AD implies Col (RCol AD,c,pD),i = pD ) :: thesis: ( i <> c implies Col (RCol AD,c,pD),i = Col AD,i )

proof

assume A2: ( i = c & len pD = len AD ) ; :: thesis: Col (RCol AD,c,pD),i = pD
then A3: ( len (RCol AD,c,pD) = len pD & width (RCol AD,c,pD) = width AD ) by Def2;
then A4: len (Col (RCol AD,c,pD),i) = len pD by MATRIX_1:def 9;

now

let J be Nat; :: thesis: ( 1 <= J & J <= len pD implies (Col (RCol AD,c,pD),i) . J = pD . J )
assume A5: ( 1 <= J & J <= len pD ) ; :: thesis: (Col (RCol AD,c,pD),i) . J = pD . J
J in NAT by ORDINAL1:def 13;
then J in Seg (len pD) by A5;
then ( J in dom (RCol AD,c,pD) & i in Seg (width (RCol AD,c,pD)) ) by A1, A3, FINSEQ_1:def 3;
then ( (Col (RCol AD,c,pD),i) . J = (RCol AD,c,pD) * J,c & [J,c] in Indices (RCol AD,c,pD) & Indices (RCol AD,c,pD) = Indices AD ) by A2, MATRIX_1:27, MATRIX_1:def 9, ZFMISC_1:106;
hence (Col (RCol AD,c,pD),i) . J = pD . J by A2, Def2; :: thesis: verum

end;

hence Col (RCol AD,c,pD),i = pD by A4, FINSEQ_1:18; :: thesis: verum

end;

assume A6: i <> c ; :: thesis: Col (RCol AD,c,pD),i = Col AD,i
A7: ( len (Col (RCol AD,c,pD),i) = len (RCol AD,c,pD) & len AD = n & len (RCol AD,c,pD) = n & len AD = len (Col AD,i) ) by MATRIX_1:def 3, MATRIX_1:def 9;

now

let j be Nat; :: thesis: ( 1 <= j & j <= len (Col AD,i) implies (Col AD,i) . b₁ = (Col (RCol AD,c,pD),i) . b₁ )
assume A8: ( 1 <= j & j <= len (Col AD,i) ) ; :: thesis: (Col AD,i) . b₁ = (Col (RCol AD,c,pD),i) . b₁
j in NAT by ORDINAL1:def 13;
then j in Seg (len AD) by A7, A8;
then ( j in dom AD & j in dom (RCol AD,c,pD) ) by A7, FINSEQ_1:def 3;
then A9: ( (Col AD,i) . j = AD * j,i & (Col (RCol AD,c,pD),i) . j = (RCol AD,c,pD) * j,i & [j,i] in Indices AD ) by A1, MATRIX_1:def 9, ZFMISC_1:106;

per cases ( len pD = len AD or len pD <> len AD ) ;

suppose len pD = len AD ; :: thesis: (Col AD,i) . b₁ = (Col (RCol AD,c,pD),i) . b₁

hence (Col AD,i) . j = (Col (RCol AD,c,pD),i) . j by A6, A9, Def2; :: thesis: verum

end;

suppose len pD <> len AD ; :: thesis: (Col AD,i) . b₁ = (Col (RCol AD,c,pD),i) . b₁

hence (Col AD,i) . j = (Col (RCol AD,c,pD),i) . j by Def2; :: thesis: verum

end;

end;

end;

hence Col (RCol AD,c,pD),i = Col AD,i by A7, FINSEQ_1:18; :: thesis: verum