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:9;

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 object ; :: 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;

then A10: card ((Seg (len A)) \ {i}) = l1 by A1, A8, STIRL2_1:55;

( 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:104;

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:27, 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

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:9;

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 object ; :: 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 :: thesis: for j being Nat st j in (dom A) \ ((Seg (len A)) \ {i}) holds

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

card (Seg (len A)) = l1 + 1
by FINSEQ_1:57;( Line (A,j) = (width A) |-> (0. K) & Line (B,j) = (width B) |-> (0. K) )

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;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

then A10: card ((Seg (len A)) \ {i}) = l1 by A1, A8, STIRL2_1:55;

( 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:104;

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:27, 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