for c, m, n being Nat
for D being non empty set
for AD being Matrix of n,m,D holds RCol (AD,c,(Col (AD,c))) = AD