let K be Field; :: thesis: for A, B being Matrix of K
for i being Nat st i in dom A & len A > 1 & Line A,i = (width A) |-> (0. K) & i in dom B & Line B,i = (width B) |-> (0. K) holds
Solutions_of A,B = Solutions_of (DelLine A,i),(DelLine B,i)
let A, B be Matrix of K; :: thesis: for i being Nat st i in dom A & len A > 1 & Line A,i = (width A) |-> (0. K) & i in dom B & Line B,i = (width B) |-> (0. K) holds
Solutions_of A,B = Solutions_of (DelLine A,i),(DelLine B,i)
let i be Nat; :: thesis: ( i in dom A & len A > 1 & Line A,i = (width A) |-> (0. K) & i in dom B & Line B,i = (width B) |-> (0. K) implies Solutions_of A,B = Solutions_of (DelLine A,i),(DelLine B,i) )
assume that
A1: ( i in dom A & len A > 1 ) and
A2: Line A,i = (width A) |-> (0. K) and
A3: ( i in dom B & Line B,i = (width B) |-> (0. K) ) ; :: thesis: Solutions_of A,B = Solutions_of (DelLine A,i),(DelLine B,i)
thus Solutions_of A,B c= Solutions_of (DelLine A,i),(DelLine B,i) by A1, Th46; :: according to XBOOLE_0:def 10 :: thesis: Solutions_of (DelLine A,i),(DelLine B,i) c= Solutions_of A,B
set S = Seg (len A);
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Solutions_of (DelLine A,i),(DelLine B,i) or x in Solutions_of A,B )
assume A4: x in Solutions_of (DelLine A,i),(DelLine B,i) ; :: thesis: x in Solutions_of A,B
consider mA being Nat such that
A5: ( len A = mA + 1 & len (Del A,i) = mA ) by A1, FINSEQ_3:113;
consider mB being Nat such that
A6: ( len B = mB + 1 & len (Del B,i) = mB ) by A3, FINSEQ_3:113;
A7: ( len B = len A & dom A = Seg (len A) ) by A4, A5, A6, Th33, FINSEQ_1:def 3;
then A8: dom A = dom B by FINSEQ_1:def 3;
reconsider l1 = (len A) - 1 as Element of NAT by A1, NAT_1:20;
A9: ( card (Seg (len A)) = l1 + 1 & (Seg (len A)) \ {i} c= Seg (len A) ) by FINSEQ_1:78, XBOOLE_1:36;
then A10: ( card ((Seg (len A)) \ {i}) = l1 & l1 > 1 - 1 ) by A1, A7, STIRL2_1:65, XREAL_1:11;

now

let j be Nat; :: thesis: ( j in (dom A) \ ((Seg (len A)) \ {i}) implies ( Line A,j = (width A) |-> (0. K) & Line B,j = (width B) |-> (0. K) ) )
assume A11: j in (dom A) \ ((Seg (len A)) \ {i}) ; :: thesis: ( Line A,j = (width A) |-> (0. K) & Line B,j = (width B) |-> (0. K) )
j in (dom A) /\ {i} by A7, A11, XBOOLE_1:48;
then j in {i} by XBOOLE_0:def 4;
hence ( Line A,j = (width A) |-> (0. K) & Line B,j = (width B) |-> (0. K) ) by A2, A3, TARSKI:def 1; :: thesis: verum

end;

then Solutions_of A,B = Solutions_of (Segm A,((Seg (len A)) \ {i}),(Seg (width A))),(Segm B,((Seg (len A)) \ {i}),(Seg (width B))) by A7, A8, A9, A10, Th45, CARD_1:47
.= Solutions_of (DelLine A,i),(Segm B,((Seg (len A)) \ {i}),(Seg (width B))) by MATRIX13:51
.= Solutions_of (DelLine A,i),(DelLine B,i) by A7, MATRIX13:51 ;
hence x in Solutions_of A,B by A4; :: thesis: verum