let c, m, n 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 :: thesis: for J being Nat st 1 <= J & J <= len pD holds
(Col ((RCol (AD,c,pD)),i)) . J = pD . J

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 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:87;
A10: Indices (RCol (AD,c,pD)) = Indices AD by MATRIX_0:26;
(Col ((RCol (AD,c,pD)),i)) . J = (RCol (AD,c,pD)) * (J,c) by A2, A8, MATRIX_0:def 8;
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_0:def 8;
hence Col ((RCol (AD,c,pD)),i) = pD by A5; :: thesis: verum

end;

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

A15: now :: thesis: for j being Nat st 1 <= j & j <= len (Col (AD,i)) holds
(Col (AD,i)) . j = (Col ((RCol (AD,c,pD)),i)) . j

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₁
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_0:def 8;
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_0:def 8;
A22: [j,i] in Indices AD by A1, A19, ZFMISC_1:87;

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_0:def 8;
hence Col ((RCol (AD,c,pD)),i) = Col (AD,i) by A11, A12, A13, A15; :: thesis: verum