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 that
A1: l in Seg n and
A2: len pK = n and
A3: 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))
set mm = the multF of K;
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 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 A4: 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,((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 A5: (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;
the multF of K $$ (Path_matrix perm,(RLine M,l,qK)) = - (the multF of K $$ (Path_matrix perm,(RLine M,l,qK))),perm by A4, MATRIX_2:def 16;
then A6: (Path_product (RLine M,l,qK)) . perm = the multF of K $$ (Path_matrix perm,(RLine M,l,qK)) by MATRIX_3:def 8;
the multF of K $$ (Path_matrix perm,(RLine M,l,pK)) = - (the multF of K $$ (Path_matrix perm,(RLine M,l,pK))),perm by A4, MATRIX_2:def 16;
then (Path_product (RLine M,l,pK)) . perm = the multF of K $$ (Path_matrix perm,(RLine M,l,pK)) 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, A2, A3, A6, A5, Th31; :: thesis: verum

end;

case A7: 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,((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 A8: (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;
- (the multF of K $$ (Path_matrix perm,(RLine M,l,pK))) = - (the multF of K $$ (Path_matrix perm,(RLine M,l,pK))),perm by A7, MATRIX_2:def 16;
then A9: (Path_product (RLine M,l,pK)) . perm = - (the multF of K $$ (Path_matrix perm,(RLine M,l,pK))) by MATRIX_3:def 8;
A10: - (a * (the multF of K $$ (Path_matrix perm,(RLine M,l,pK)))) = a * (- (the multF of K $$ (Path_matrix perm,(RLine M,l,pK)))) by VECTSP_1:40;
- (the multF of K $$ (Path_matrix perm,(RLine M,l,qK))) = - (the multF of K $$ (Path_matrix perm,(RLine M,l,qK))),perm by A7, MATRIX_2:def 16;
then A11: (Path_product (RLine M,l,qK)) . perm = - (the multF of K $$ (Path_matrix perm,(RLine M,l,qK))) by MATRIX_3:def 8;
A12: - ((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:64;
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, A2, A3, Th31;
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 A9, A11, A8, A10, A12, VECTSP_1:40; :: 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