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) )
assume A1: [:P,Q:] c= Indices A ; :: thesis: Segm (A + B),P,Q = (Segm A,P,Q) + (Segm B,P,Q)
consider n being Nat such that
A2: P c= Seg n by MATRIX13:43;
consider m being Nat such that
A3: Q c= Seg m by MATRIX13:43;
( rng (Sgm P) = P & rng (Sgm Q) = Q ) by A2, A3, FINSEQ_1:def 13;
hence Segm (A + B),P,Q = (Segm A,P,Q) + (Segm B,P,Q) by A1, Th1; :: thesis: verum