:: deftheorem Def3 defines ReplaceLine MATRIX11:def 3 :
for l, 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 = width M implies ( b₇ = ReplaceLine (M,l,pD) iff ( len b₇ = len M & width b₇ = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i <> l implies b₇ * (i,j) = M * (i,j) ) & ( i = l implies b₇ * (l,j) = pD . j ) ) ) ) ) ) & ( not len pD = width M implies ( b₇ = ReplaceLine (M,l,pD) iff b₇ = M ) ) );