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 & not N is empty & dom A = dom B ) and
A2: 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) & card N <> 0 ) by A1, FINSEQ_1:def 3;
then ( rng (Sgm N) = N & card N > 0 ) 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