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 )
assume A1: [:P,Q:] c= Indices M ; :: thesis: a * (Segm M,P,Q) = Segm (a * M),P,Q
consider n being Nat such that
A2: P c= Seg n by Th43;
consider k being Nat such that
A3: Q c= Seg k by Th43;
( rng (Sgm P) = P & rng (Sgm Q) = Q ) by A2, A3, FINSEQ_1:def 13;
hence a * (Segm M,P,Q) = Segm (a * M),P,Q by A1, Th41; :: thesis: verum