:: deftheorem Def2 defines ReplaceCol LAPLACE:def 2 :
for c, n, m being Nat
for D being non empty set
for M being Matrix of n,m,D
for pD being FinSequence of D
for b₇ being Matrix of n,m,D holds
( ( len pD = len M implies ( b₇ = ReplaceCol (M,c,pD) iff ( len b₇ = len M & width b₇ = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( j <> c implies b₇ * (i,j) = M * (i,j) ) & ( j = c implies b₇ * (i,c) = pD . i ) ) ) ) ) ) & ( not len pD = len M implies ( b₇ = ReplaceCol (M,c,pD) iff b₇ = M ) ) );