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 and
A2: len A > 1 and
A3: Line A,i = (width A) |-> (0. K) and
A4: i in dom B and
A5: Line B,i = (width B) |-> (0. K) ; :: thesis: Solutions_of A,B = Solutions_of (DelLine A,i),(DelLine B,i)
reconsider l1 = (len A) - 1 as Element of NAT by A2, NAT_1:20;
A6: l1 > 1 - 1 by A2, XREAL_1:11;
thus Solutions_of A,B c= Solutions_of (DelLine A,i),(DelLine B,i) by A1, A2, Th46; :: according to XBOOLE_0:def 10 :: thesis: Solutions_of (DelLine A,i),(DelLine B,i) c= Solutions_of A,B
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 A7: x in Solutions_of (DelLine A,i),(DelLine B,i) ; :: thesis: x in Solutions_of A,B
set S = Seg (len A);
A8: dom A = Seg (len A) by FINSEQ_1:def 3;

A9: 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 j in (dom A) \ ((Seg (len A)) \ {i}) ; :: thesis: ( Line A,j = (width A) |-> (0. K) & Line B,j = (width B) |-> (0. K) )
then j in (dom A) /\ {i} by A8, 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 A3, A5, TARSKI:def 1; :: thesis: verum

end;

card (Seg (len A)) = l1 + 1 by FINSEQ_1:78;
then A10: card ((Seg (len A)) \ {i}) = l1 by A1, A8, STIRL2_1:65;
( ex mA being Nat st
( len A = mA + 1 & len (Del A,i) = mA ) & ex mB being Nat st
( len B = mB + 1 & len (Del B,i) = mB ) ) by A1, A4, FINSEQ_3:113;
then A11: len B = len A by A7, Th33;
then dom A = dom B by A8, FINSEQ_1:def 3;
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 A8, A10, A6, A9, Th45, CARD_1:47, XBOOLE_1:36
.= 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 A11, MATRIX13:51 ;
hence x in Solutions_of A,B by A7; :: thesis: verum