for c, m, n being Nat
for D being non empty set
for pD being FinSequence of D
for A being Matrix of n,m,D
for A9 being Matrix of m,n,D st A9 = A @ & ( m = 0 implies n = 0 ) holds
ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @