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:11;
A4: Seg (len A) = dom A by FINSEQ_1:def 3;
card (Seg (len A)) = l1 + 1 by FINSEQ_1:78;
then card ((Seg (len A)) \ {i}) = l1 by A1, A4, STIRL2_1:65;
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:47, XBOOLE_1:36;
let x be set ; :: 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