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