let K be Field; :: thesis: for a being Element of K
for M being Matrix of K
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M holds
a * (Segm (M,P,Q)) = Segm ((a * M),P,Q)
let a be Element of K; :: thesis: for M being Matrix of K
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M holds
a * (Segm (M,P,Q)) = Segm ((a * M),P,Q)
let M be Matrix of K; :: thesis: for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M holds
a * (Segm (M,P,Q)) = Segm ((a * M),P,Q)
let P, Q be finite without_zero Subset of NAT; :: thesis: ( [:P,Q:] c= Indices M implies a * (Segm (M,P,Q)) = Segm ((a * M),P,Q) )
( rng (Sgm P) = P & rng (Sgm Q) = Q ) by FINSEQ_1:def 14;
hence ( [:P,Q:] c= Indices M implies a * (Segm (M,P,Q)) = Segm ((a * M),P,Q) ) by Th41; :: thesis: verum