let K be Field; :: thesis: for A, B being Matrix of K
for N being finite without_zero Subset of NAT st N c= dom A & not N is empty holds
Solutions_of (A,B) c= Solutions_of ((Segm (A,N,(Seg (width A)))),(Segm (B,N,(Seg (width B)))))
let A, B be Matrix of K; :: thesis: for N being finite without_zero Subset of NAT st N c= dom A & not N is empty holds
Solutions_of (A,B) c= Solutions_of ((Segm (A,N,(Seg (width A)))),(Segm (B,N,(Seg (width B)))))
let N be finite without_zero Subset of NAT; :: thesis: ( N c= dom A & not N is empty implies Solutions_of (A,B) c= Solutions_of ((Segm (A,N,(Seg (width A)))),(Segm (B,N,(Seg (width B))))) )
assume that
A1: N c= dom A and
A2: not N is empty ; :: thesis: Solutions_of (A,B) c= Solutions_of ((Segm (A,N,(Seg (width A)))),(Segm (B,N,(Seg (width B)))))
dom A = Seg (len A) by FINSEQ_1:def 3;
then rng (Sgm N) = N by A1, FINSEQ_1:def 13;
hence Solutions_of (A,B) c= Solutions_of ((Segm (A,N,(Seg (width A)))),(Segm (B,N,(Seg (width B))))) by A1, A2, Th42; :: thesis: verum