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;
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 that
A2: i = c and
A3: len pD = len AD ; :: thesis: Col (RCol AD,c,pD),i = pD
A4: len (RCol AD,c,pD) = len pD by A3, Def2;

A5: now

let J be Nat; :: thesis: ( 1 <= J & J <= len pD implies (Col (RCol AD,c,pD),i) . J = pD . J )
assume that
A6: 1 <= J and
A7: 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 A6, A7;
then A8: J in dom (RCol AD,c,pD) by A4, FINSEQ_1:def 3;
i in Seg (width (RCol AD,c,pD)) by A1, A3, Def2;
then A9: [J,c] in Indices (RCol AD,c,pD) by A2, A8, ZFMISC_1:106;
A10: Indices (RCol AD,c,pD) = Indices AD by MATRIX_1:27;
(Col (RCol AD,c,pD),i) . J = (RCol AD,c,pD) * J,c by A2, A8, MATRIX_1:def 9;
hence (Col (RCol AD,c,pD),i) . J = pD . J by A3, A9, A10, Def2; :: thesis: verum

end;

len (Col (RCol AD,c,pD),i) = len pD by A4, MATRIX_1:def 9;
hence Col (RCol AD,c,pD),i = pD by A5, FINSEQ_1:18; :: thesis: verum

end;

set CA = Col AD,i;
A11: len AD = n by MATRIX_1:def 3;
A12: len (RCol AD,c,pD) = n by MATRIX_1:def 3;
A13: len AD = len (Col AD,i) by MATRIX_1:def 9;
assume A14: i <> c ; :: thesis: Col (RCol AD,c,pD),i = Col AD,i

A15: 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 that
A16: 1 <= j and
A17: 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 A18: j in Seg (len AD) by A13, A16, A17;
then A19: j in dom AD by FINSEQ_1:def 3;
then A20: (Col AD,i) . j = AD * j,i by MATRIX_1:def 9;
j in dom (RCol AD,c,pD) by A11, A12, A18, FINSEQ_1:def 3;
then A21: (Col (RCol AD,c,pD),i) . j = (RCol AD,c,pD) * j,i by MATRIX_1:def 9;
A22: [j,i] in Indices AD by A1, A19, 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 A14, A20, A21, A22, 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;

len (Col (RCol AD,c,pD),i) = len (RCol AD,c,pD) by MATRIX_1:def 9;
hence Col (RCol AD,c,pD),i = Col AD,i by A11, A12, A13, A15, FINSEQ_1:18; :: thesis: verum