theorem Th31:
for
n being
Nat for
K being
commutative Ring for
a,
b being
Element of
K for
l being
Nat for
pK,
qK being
FinSequence of
K for
perm being
Element of
Permutations n st
l in Seg n &
len pK = n &
len qK = n holds
for
M being
Matrix of
n,
K holds the
multF of
K $$ (Path_matrix (perm,(RLine (M,l,((a * pK) + (b * qK)))))) = (a * ( the multF of K $$ (Path_matrix (perm,(RLine (M,l,pK)))))) + (b * ( the multF of K $$ (Path_matrix (perm,(RLine (M,l,qK))))))