let n, m, c be Nat; :: thesis: for D being non empty set
for AD being Matrix of n,m,D holds RCol AD,c,(Col AD,c) = AD
let D be non empty set ; :: thesis: for AD being Matrix of n,m,D holds RCol AD,c,(Col AD,c) = AD
let AD be Matrix of n,m,D; :: thesis: RCol AD,c,(Col AD,c) = AD
set C = Col AD,c;
set R = RCol AD,c,(Col AD,c);

now

reconsider c = c as Element of NAT by ORDINAL1:def 13;
let i, j be Nat; :: thesis: ( [i,j] in Indices AD implies (RCol AD,c,(Col AD,c)) * i,j = AD * i,j )
assume A1: [i,j] in Indices AD ; :: thesis: (RCol AD,c,(Col AD,c)) * i,j = AD * i,j
A2: len (Col AD,c) = len AD by MATRIX_1:def 9;
reconsider I = i, J = j as Element of NAT by ORDINAL1:def 13;
A3: i in dom AD by A1, ZFMISC_1:106;

now

per cases ( c = j or c <> J ) ;

suppose A4: c = j ; :: thesis: (RCol AD,c,(Col AD,c)) * i,j = AD * i,j

hence (RCol AD,c,(Col AD,c)) * i,j = (Col AD,c) . I by A1, A2, Def2
.= AD * i,j by A3, A4, MATRIX_1:def 9 ;
:: thesis: verum

end;

suppose c <> J ; :: thesis: (RCol AD,c,(Col AD,c)) * i,j = AD * i,j

hence (RCol AD,c,(Col AD,c)) * i,j = AD * i,j by A1, A2, Def2; :: thesis: verum

end;

end;

end;

hence (RCol AD,c,(Col AD,c)) * i,j = AD * i,j ; :: thesis: verum

end;

hence RCol AD,c,(Col AD,c) = AD by MATRIX_1:28; :: thesis: verum