let n be Nat; :: thesis: for K being Field
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 (Path_product (RLine M,l,((a * pK) + (b * qK)))) . perm = (a * ((Path_product (RLine M,l,pK)) . perm)) + (b * ((Path_product (RLine M,l,qK)) . perm))
let K be Field; :: thesis: 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 (Path_product (RLine M,l,((a * pK) + (b * qK)))) . perm = (a * ((Path_product (RLine M,l,pK)) . perm)) + (b * ((Path_product (RLine M,l,qK)) . perm))
let a, b be Element of K; :: thesis: 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 (Path_product (RLine M,l,((a * pK) + (b * qK)))) . perm = (a * ((Path_product (RLine M,l,pK)) . perm)) + (b * ((Path_product (RLine M,l,qK)) . perm))
let l be Nat; :: thesis: 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 (Path_product (RLine M,l,((a * pK) + (b * qK)))) . perm = (a * ((Path_product (RLine M,l,pK)) . perm)) + (b * ((Path_product (RLine M,l,qK)) . perm))
let pK, qK be FinSequence of K; :: thesis: 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 (Path_product (RLine M,l,((a * pK) + (b * qK)))) . perm = (a * ((Path_product (RLine M,l,pK)) . perm)) + (b * ((Path_product (RLine M,l,qK)) . perm))
let perm be Element of Permutations n; :: thesis: ( l in Seg n & len pK = n & len qK = n implies for M being Matrix of n,K holds (Path_product (RLine M,l,((a * pK) + (b * qK)))) . perm = (a * ((Path_product (RLine M,l,pK)) . perm)) + (b * ((Path_product (RLine M,l,qK)) . perm)) )
assume A1: ( l in Seg n & len pK = n & len qK = n ) ; :: thesis: for M being Matrix of n,K holds (Path_product (RLine M,l,((a * pK) + (b * qK)))) . perm = (a * ((Path_product (RLine M,l,pK)) . perm)) + (b * ((Path_product (RLine M,l,qK)) . perm))
let M be Matrix of n,K; :: thesis: (Path_product (RLine M,l,((a * pK) + (b * qK)))) . perm = (a * ((Path_product (RLine M,l,pK)) . perm)) + (b * ((Path_product (RLine M,l,qK)) . perm))
set mm = the multF of K;
set Rpq = RLine M,l,((a * pK) + (b * qK));
set Rp = RLine M,l,pK;
set Rq = RLine M,l,qK;
set Ppq = Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)));
set Pathpq = Path_product (RLine M,l,((a * pK) + (b * qK)));
set Pp = Path_matrix perm,(RLine M,l,pK);
set Pathp = Path_product (RLine M,l,pK);
set Pq = Path_matrix perm,(RLine M,l,qK);
set Pathq = Path_product (RLine M,l,qK);

now

per cases ( perm is even or not perm is even ) ;

case perm is even ; :: thesis: (Path_product (RLine M,l,((a * pK) + (b * qK)))) . perm = (a * ((Path_product (RLine M,l,pK)) . perm)) + (b * ((Path_product (RLine M,l,qK)) . perm))

then ( the multF of K $$ (Path_matrix perm,(RLine M,l,pK)) = - (the multF of K $$ (Path_matrix perm,(RLine M,l,pK))),perm & the multF of K $$ (Path_matrix perm,(RLine M,l,qK)) = - (the multF of K $$ (Path_matrix perm,(RLine M,l,qK))),perm & the multF of K $$ (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) = - (the multF of K $$ (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK))))),perm ) by MATRIX_2:def 16;
then ( (Path_product (RLine M,l,pK)) . perm = the multF of K $$ (Path_matrix perm,(RLine M,l,pK)) & (Path_product (RLine M,l,qK)) . perm = the multF of K $$ (Path_matrix perm,(RLine M,l,qK)) & (Path_product (RLine M,l,((a * pK) + (b * qK)))) . perm = the multF of K $$ (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK)))) ) by MATRIX_3:def 8;
hence (Path_product (RLine M,l,((a * pK) + (b * qK)))) . perm = (a * ((Path_product (RLine M,l,pK)) . perm)) + (b * ((Path_product (RLine M,l,qK)) . perm)) by A1, Th31; :: thesis: verum

end;

case not perm is even ; :: thesis: (Path_product (RLine M,l,((a * pK) + (b * qK)))) . perm = (a * ((Path_product (RLine M,l,pK)) . perm)) + (b * ((Path_product (RLine M,l,qK)) . perm))

then ( - (the multF of K $$ (Path_matrix perm,(RLine M,l,pK))) = - (the multF of K $$ (Path_matrix perm,(RLine M,l,pK))),perm & - (the multF of K $$ (Path_matrix perm,(RLine M,l,qK))) = - (the multF of K $$ (Path_matrix perm,(RLine M,l,qK))),perm & - (the multF of K $$ (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK))))) = - (the multF of K $$ (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK))))),perm ) by MATRIX_2:def 16;
then A2: ( (Path_product (RLine M,l,pK)) . perm = - (the multF of K $$ (Path_matrix perm,(RLine M,l,pK))) & (Path_product (RLine M,l,qK)) . perm = - (the multF of K $$ (Path_matrix perm,(RLine M,l,qK))) & (Path_product (RLine M,l,((a * pK) + (b * qK)))) . perm = - (the multF of K $$ (Path_matrix perm,(RLine M,l,((a * pK) + (b * qK))))) & 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)))) ) by A1, Th31, MATRIX_3:def 8;
( - (a * (the multF of K $$ (Path_matrix perm,(RLine M,l,pK)))) = a * (- (the multF of K $$ (Path_matrix perm,(RLine M,l,pK)))) & - (b * (the multF of K $$ (Path_matrix perm,(RLine M,l,qK)))) = b * (- (the multF of K $$ (Path_matrix perm,(RLine M,l,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))))) = (- (a * (the multF of K $$ (Path_matrix perm,(RLine M,l,pK))))) - (b * (the multF of K $$ (Path_matrix perm,(RLine M,l,qK)))) ) by VECTSP_1:40, VECTSP_1:64;
hence (Path_product (RLine M,l,((a * pK) + (b * qK)))) . perm = (a * ((Path_product (RLine M,l,pK)) . perm)) + (b * ((Path_product (RLine M,l,qK)) . perm)) by A2; :: thesis: verum

end;

end;

end;

hence (Path_product (RLine M,l,((a * pK) + (b * qK)))) . perm = (a * ((Path_product (RLine M,l,pK)) . perm)) + (b * ((Path_product (RLine M,l,qK)) . perm)) ; :: thesis: verum