let K be Field; 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; 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; ( 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)
; 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; XBOOLE_0:def 10 Solutions_of ((DelLine (A,i)),(DelLine (B,i))) c= Solutions_of (A,B)
let x be object ; TARSKI:def 3 ( 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)))
; x in Solutions_of (A,B)
set S = Seg (len A);
A8:
dom A = Seg (len A)
by FINSEQ_1:def 3;
card (Seg (len A)) = l1 + 1
by FINSEQ_1:57;
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; verum