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

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
reconsider I = i, J = j as Element of NAT by ORDINAL1:def 13;
A2: ( i in dom AD & len (Col AD,c) = len AD ) by A1, MATRIX_1:def 9, ZFMISC_1:106;
reconsider c = c as Element of NAT by ORDINAL1:def 13;

now

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

suppose A3: 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 A2, A3, 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