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 & dom A = dom B & ( for i being Nat st i in (dom A) \ N holds

( Line (A,i) = (width A) |-> (0. K) & Line (B,i) = (width B) |-> (0. K) ) ) holds

Solutions_of (A,B) = 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 & dom A = dom B & ( for i being Nat st i in (dom A) \ N holds

( Line (A,i) = (width A) |-> (0. K) & Line (B,i) = (width B) |-> (0. K) ) ) holds

Solutions_of (A,B) = 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 & dom A = dom B & ( for i being Nat st i in (dom A) \ N holds

( Line (A,i) = (width A) |-> (0. K) & Line (B,i) = (width B) |-> (0. K) ) ) implies Solutions_of (A,B) = 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 & dom A = dom B & ( for i being Nat st i in (dom A) \ N holds

( Line (A,i) = (width A) |-> (0. K) & Line (B,i) = (width B) |-> (0. K) ) ) ) ; :: thesis: Solutions_of (A,B) = 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) = Solutions_of ((Segm (A,N,(Seg (width A)))),(Segm (B,N,(Seg (width B))))) by A1, A2, Th43; :: thesis: verum

for N being finite without_zero Subset of NAT st N c= dom A & not N is empty & dom A = dom B & ( for i being Nat st i in (dom A) \ N holds

( Line (A,i) = (width A) |-> (0. K) & Line (B,i) = (width B) |-> (0. K) ) ) holds

Solutions_of (A,B) = 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 & dom A = dom B & ( for i being Nat st i in (dom A) \ N holds

( Line (A,i) = (width A) |-> (0. K) & Line (B,i) = (width B) |-> (0. K) ) ) holds

Solutions_of (A,B) = 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 & dom A = dom B & ( for i being Nat st i in (dom A) \ N holds

( Line (A,i) = (width A) |-> (0. K) & Line (B,i) = (width B) |-> (0. K) ) ) implies Solutions_of (A,B) = 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 & dom A = dom B & ( for i being Nat st i in (dom A) \ N holds

( Line (A,i) = (width A) |-> (0. K) & Line (B,i) = (width B) |-> (0. K) ) ) ) ; :: thesis: Solutions_of (A,B) = 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) = Solutions_of ((Segm (A,N,(Seg (width A)))),(Segm (B,N,(Seg (width B))))) by A1, A2, Th43; :: thesis: verum