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) )

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)

hence Col ((RCol (AD,c,pD)),i) = Col (AD,i) by A11, A12, A13, A15; :: thesis: verum

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

set CA = Col (AD,i);
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;

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

end;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

len (Col ((RCol (AD,c,pD)),i)) = len pD
by A4, MATRIX_0:def 8;(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;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

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

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

len (Col ((RCol (AD,c,pD)),i)) = len (RCol (AD,c,pD))
by MATRIX_0:def 8;(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_{1} = (Col ((RCol (AD,c,pD)),i)) . b_{1} )

assume that

A16: 1 <= j and

A17: j <= len (Col (AD,i)) ; :: thesis: (Col (AD,i)) . b_{1} = (Col ((RCol (AD,c,pD)),i)) . b_{1}

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;

end;assume that

A16: 1 <= j and

A17: j <= len (Col (AD,i)) ; :: thesis: (Col (AD,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;

hence Col ((RCol (AD,c,pD)),i) = Col (AD,i) by A11, A12, A13, A15; :: thesis: verum