let i be Nat; :: thesis: for K being Field

for A, B being Matrix of K st i in dom A & len A > 1 holds

Solutions_of (A,B) c= Solutions_of ((DelLine (A,i)),(DelLine (B,i)))

let K be Field; :: thesis: for A, B being Matrix of K st i in dom A & len A > 1 holds

Solutions_of (A,B) c= Solutions_of ((DelLine (A,i)),(DelLine (B,i)))

let A, B be Matrix of K; :: thesis: ( i in dom A & len A > 1 implies Solutions_of (A,B) c= Solutions_of ((DelLine (A,i)),(DelLine (B,i))) )

assume that

A1: i in dom A and

A2: len A > 1 ; :: thesis: Solutions_of (A,B) c= Solutions_of ((DelLine (A,i)),(DelLine (B,i)))

reconsider l1 = (len A) - 1 as Element of NAT by A2, NAT_1:20;

A3: l1 > 1 - 1 by A2, XREAL_1:9;

A4: Seg (len A) = dom A by FINSEQ_1:def 3;

card (Seg (len A)) = l1 + 1 by FINSEQ_1:57;

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

then A5: Solutions_of (A,B) c= Solutions_of ((Segm (A,((Seg (len A)) \ {i}),(Seg (width A)))),(Segm (B,((Seg (len A)) \ {i}),(Seg (width B))))) by A4, A3, Th44, CARD_1:27, XBOOLE_1:36;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Solutions_of (A,B) or x in Solutions_of ((DelLine (A,i)),(DelLine (B,i))) )

assume A6: x in Solutions_of (A,B) ; :: thesis: x in Solutions_of ((DelLine (A,i)),(DelLine (B,i)))

len A = len B by A6, Th33;

then ( Segm (A,((Seg (len A)) \ {i}),(Seg (width A))) = Del (A,i) & Segm (B,((Seg (len A)) \ {i}),(Seg (width B))) = Del (B,i) ) by MATRIX13:51;

hence x in Solutions_of ((DelLine (A,i)),(DelLine (B,i))) by A5, A6; :: thesis: verum

for A, B being Matrix of K st i in dom A & len A > 1 holds

Solutions_of (A,B) c= Solutions_of ((DelLine (A,i)),(DelLine (B,i)))

let K be Field; :: thesis: for A, B being Matrix of K st i in dom A & len A > 1 holds

Solutions_of (A,B) c= Solutions_of ((DelLine (A,i)),(DelLine (B,i)))

let A, B be Matrix of K; :: thesis: ( i in dom A & len A > 1 implies Solutions_of (A,B) c= Solutions_of ((DelLine (A,i)),(DelLine (B,i))) )

assume that

A1: i in dom A and

A2: len A > 1 ; :: thesis: Solutions_of (A,B) c= Solutions_of ((DelLine (A,i)),(DelLine (B,i)))

reconsider l1 = (len A) - 1 as Element of NAT by A2, NAT_1:20;

A3: l1 > 1 - 1 by A2, XREAL_1:9;

A4: Seg (len A) = dom A by FINSEQ_1:def 3;

card (Seg (len A)) = l1 + 1 by FINSEQ_1:57;

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

then A5: Solutions_of (A,B) c= Solutions_of ((Segm (A,((Seg (len A)) \ {i}),(Seg (width A)))),(Segm (B,((Seg (len A)) \ {i}),(Seg (width B))))) by A4, A3, Th44, CARD_1:27, XBOOLE_1:36;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Solutions_of (A,B) or x in Solutions_of ((DelLine (A,i)),(DelLine (B,i))) )

assume A6: x in Solutions_of (A,B) ; :: thesis: x in Solutions_of ((DelLine (A,i)),(DelLine (B,i)))

len A = len B by A6, Th33;

then ( Segm (A,((Seg (len A)) \ {i}),(Seg (width A))) = Del (A,i) & Segm (B,((Seg (len A)) \ {i}),(Seg (width B))) = Del (B,i) ) by MATRIX13:51;

hence x in Solutions_of ((DelLine (A,i)),(DelLine (B,i))) by A5, A6; :: thesis: verum