let K be Field; 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; 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; ( [: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
; Segm ((A + B),P,Q) = (Segm (A,P,Q)) + (Segm (B,P,Q))
ex m being Nat st Q c= Seg m
by MATRIX13:43;
then A2:
rng (Sgm Q) = Q
by FINSEQ_1:def 13;
ex n being Nat st P c= Seg n
by MATRIX13:43;
then
rng (Sgm P) = P
by FINSEQ_1:def 13;
hence
Segm ((A + B),P,Q) = (Segm (A,P,Q)) + (Segm (B,P,Q))
by A1, A2, Th1; verum