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

for A, B being Matrix of K

for nt being Element of n -tuples_on NAT st rng nt c= dom A & dom A = dom B & n > 0 & ( for i being Nat st i in (dom A) \ (rng nt) holds

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

Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B))))))

let K be Field; :: thesis: for A, B being Matrix of K

for nt being Element of n -tuples_on NAT st rng nt c= dom A & dom A = dom B & n > 0 & ( for i being Nat st i in (dom A) \ (rng nt) holds

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

Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B))))))

let A, B be Matrix of K; :: thesis: for nt being Element of n -tuples_on NAT st rng nt c= dom A & dom A = dom B & n > 0 & ( for i being Nat st i in (dom A) \ (rng nt) holds

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

Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B))))))

let nt be Element of n -tuples_on NAT; :: thesis: ( rng nt c= dom A & dom A = dom B & n > 0 & ( for i being Nat st i in (dom A) \ (rng nt) holds

( Line (A,i) = (width A) |-> (0. K) & Line (B,i) = (width B) |-> (0. K) ) ) implies Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B)))))) )

assume that

A1: rng nt c= dom A and

A2: dom A = dom B and

A3: n > 0 and

A4: for i being Nat st i in (dom A) \ (rng nt) holds

( Line (A,i) = (width A) |-> (0. K) & Line (B,i) = (width B) |-> (0. K) ) ; :: thesis: Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B))))))

set SB = Segm (B,nt,(Sgm (Seg (width B))));

set SA = Segm (A,nt,(Sgm (Seg (width A))));

A5: Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B)))))) c= Solutions_of (A,B)

hence Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B)))))) by A5; :: thesis: verum

for A, B being Matrix of K

for nt being Element of n -tuples_on NAT st rng nt c= dom A & dom A = dom B & n > 0 & ( for i being Nat st i in (dom A) \ (rng nt) holds

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

Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B))))))

let K be Field; :: thesis: for A, B being Matrix of K

for nt being Element of n -tuples_on NAT st rng nt c= dom A & dom A = dom B & n > 0 & ( for i being Nat st i in (dom A) \ (rng nt) holds

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

Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B))))))

let A, B be Matrix of K; :: thesis: for nt being Element of n -tuples_on NAT st rng nt c= dom A & dom A = dom B & n > 0 & ( for i being Nat st i in (dom A) \ (rng nt) holds

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

Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B))))))

let nt be Element of n -tuples_on NAT; :: thesis: ( rng nt c= dom A & dom A = dom B & n > 0 & ( for i being Nat st i in (dom A) \ (rng nt) holds

( Line (A,i) = (width A) |-> (0. K) & Line (B,i) = (width B) |-> (0. K) ) ) implies Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B)))))) )

assume that

A1: rng nt c= dom A and

A2: dom A = dom B and

A3: n > 0 and

A4: for i being Nat st i in (dom A) \ (rng nt) holds

( Line (A,i) = (width A) |-> (0. K) & Line (B,i) = (width B) |-> (0. K) ) ; :: thesis: Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B))))))

set SB = Segm (B,nt,(Sgm (Seg (width B))));

set SA = Segm (A,nt,(Sgm (Seg (width A))));

A5: Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B)))))) c= Solutions_of (A,B)

proof

Solutions_of (A,B) c= Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B))))))
by A1, A3, Th42;
A6:
Seg (len A) = dom B
by A2, FINSEQ_1:def 3;

A7: width (Segm (B,nt,(Sgm (Seg (width B))))) = card (Seg (width B)) by A3, MATRIX_0:23;

then A8: width (Segm (B,nt,(Sgm (Seg (width B))))) = width B by FINSEQ_1:57;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B)))))) or x in Solutions_of (A,B) )

assume x in Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B)))))) ; :: thesis: x in Solutions_of (A,B)

then consider X being Matrix of K such that

A9: x = X and

A10: len X = width (Segm (A,nt,(Sgm (Seg (width A))))) and

A11: width X = width (Segm (B,nt,(Sgm (Seg (width B))))) and

A12: (Segm (A,nt,(Sgm (Seg (width A))))) * X = Segm (B,nt,(Sgm (Seg (width B)))) ;

set AX = A * X;

width (Segm (A,nt,(Sgm (Seg (width A))))) = card (Seg (width A)) by A3, MATRIX_0:23;

then A13: width (Segm (A,nt,(Sgm (Seg (width A))))) = width A by FINSEQ_1:57;

then A14: width (A * X) = width X by A10, MATRIX_3:def 4;

A15: len (A * X) = len A by A10, A13, MATRIX_3:def 4;

then A * X = B by A11, A7, A14, A16, FINSEQ_1:57, MATRIX_0:21;

hence x in Solutions_of (A,B) by A9, A10, A11, A13, A8; :: thesis: verum

end;A7: width (Segm (B,nt,(Sgm (Seg (width B))))) = card (Seg (width B)) by A3, MATRIX_0:23;

then A8: width (Segm (B,nt,(Sgm (Seg (width B))))) = width B by FINSEQ_1:57;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B)))))) or x in Solutions_of (A,B) )

assume x in Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B)))))) ; :: thesis: x in Solutions_of (A,B)

then consider X being Matrix of K such that

A9: x = X and

A10: len X = width (Segm (A,nt,(Sgm (Seg (width A))))) and

A11: width X = width (Segm (B,nt,(Sgm (Seg (width B))))) and

A12: (Segm (A,nt,(Sgm (Seg (width A))))) * X = Segm (B,nt,(Sgm (Seg (width B)))) ;

set AX = A * X;

width (Segm (A,nt,(Sgm (Seg (width A))))) = card (Seg (width A)) by A3, MATRIX_0:23;

then A13: width (Segm (A,nt,(Sgm (Seg (width A))))) = width A by FINSEQ_1:57;

then A14: width (A * X) = width X by A10, MATRIX_3:def 4;

A15: len (A * X) = len A by A10, A13, MATRIX_3:def 4;

A16: now :: thesis: for j, k being Nat st [j,k] in Indices (A * X) holds

(A * X) * (j,k) = B * (j,k)

len (A * X) = len B
by A15, A6, FINSEQ_1:def 3;(A * X) * (j,k) = B * (j,k)

A17:
dom (A * X) = Seg (len A)
by A15, FINSEQ_1:def 3;

let j, k be Nat; :: thesis: ( [j,k] in Indices (A * X) implies (A * X) * (j,k) = B * (j,k) )

assume A18: [j,k] in Indices (A * X) ; :: thesis: (A * X) * (j,k) = B * (j,k)

A19: k in Seg (width (A * X)) by A18, ZFMISC_1:87;

reconsider j9 = j, k9 = k as Element of NAT by ORDINAL1:def 12;

A20: j in dom (A * X) by A18, ZFMISC_1:87;

end;let j, k be Nat; :: thesis: ( [j,k] in Indices (A * X) implies (A * X) * (j,k) = B * (j,k) )

assume A18: [j,k] in Indices (A * X) ; :: thesis: (A * X) * (j,k) = B * (j,k)

A19: k in Seg (width (A * X)) by A18, ZFMISC_1:87;

reconsider j9 = j, k9 = k as Element of NAT by ORDINAL1:def 12;

A20: j in dom (A * X) by A18, ZFMISC_1:87;

now :: thesis: (A * X) * (j,k) = B * (j,k)end;

hence
(A * X) * (j,k) = B * (j,k)
; :: thesis: verumper cases
( j9 in rng nt or not j9 in rng nt )
;

end;

suppose A21:
j9 in rng nt
; :: thesis: (A * X) * (j,k) = B * (j,k)

A22:
dom nt = Seg n
by FINSEQ_2:124;

Sgm (Seg (width B)) = idseq (width B) by FINSEQ_3:48;

then A23: (Sgm (Seg (width B))) . k9 = k by A11, A8, A14, A19, FINSEQ_2:49;

consider p being object such that

A24: p in dom nt and

A25: nt . p = j9 by A21, FUNCT_1:def 3;

reconsider p = p as Element of NAT by A24;

Indices (Segm (B,nt,(Sgm (Seg (width B))))) = [:(Seg n),(Seg (card (Seg (width B)))):] by A3, MATRIX_0:23;

then A26: [p,k] in Indices (Segm (B,nt,(Sgm (Seg (width B))))) by A11, A7, A14, A19, A24, A22, ZFMISC_1:87;

Line ((Segm (A,nt,(Sgm (Seg (width A))))),p) = Line (A,j9) by A24, A25, A22, Lm6;

hence (A * X) * (j,k) = (Line ((Segm (A,nt,(Sgm (Seg (width A))))),p)) "*" (Col (X,k)) by A10, A13, A18, MATRIX_3:def 4

.= (Segm (B,nt,(Sgm (Seg (width B))))) * (p,k9) by A10, A12, A26, MATRIX_3:def 4

.= B * (j,k) by A25, A26, A23, MATRIX13:def 1 ;

:: thesis: verum

end;Sgm (Seg (width B)) = idseq (width B) by FINSEQ_3:48;

then A23: (Sgm (Seg (width B))) . k9 = k by A11, A8, A14, A19, FINSEQ_2:49;

consider p being object such that

A24: p in dom nt and

A25: nt . p = j9 by A21, FUNCT_1:def 3;

reconsider p = p as Element of NAT by A24;

Indices (Segm (B,nt,(Sgm (Seg (width B))))) = [:(Seg n),(Seg (card (Seg (width B)))):] by A3, MATRIX_0:23;

then A26: [p,k] in Indices (Segm (B,nt,(Sgm (Seg (width B))))) by A11, A7, A14, A19, A24, A22, ZFMISC_1:87;

Line ((Segm (A,nt,(Sgm (Seg (width A))))),p) = Line (A,j9) by A24, A25, A22, Lm6;

hence (A * X) * (j,k) = (Line ((Segm (A,nt,(Sgm (Seg (width A))))),p)) "*" (Col (X,k)) by A10, A13, A18, MATRIX_3:def 4

.= (Segm (B,nt,(Sgm (Seg (width B))))) * (p,k9) by A10, A12, A26, MATRIX_3:def 4

.= B * (j,k) by A25, A26, A23, MATRIX13:def 1 ;

:: thesis: verum

suppose
not j9 in rng nt
; :: thesis: (A * X) * (j,k) = B * (j,k)

then A27:
j9 in (dom A) \ (rng nt)
by A2, A6, A20, A17, XBOOLE_0:def 5;

then A28: Line (B,j) = (width B) |-> (0. K) by A4;

Line (A,j) = (width A) |-> (0. K) by A4, A27;

hence (A * X) * (j,k) = ((width A) |-> (0. K)) "*" (Col (X,k)) by A10, A13, A18, MATRIX_3:def 4

.= Sum ((0. K) * (Col (X,k))) by A10, A13, FVSUM_1:66

.= (0. K) * (Sum (Col (X,k))) by FVSUM_1:73

.= 0. K

.= (Line (B,j)) . k by A11, A8, A14, A19, A28, FINSEQ_2:57

.= B * (j,k) by A11, A8, A14, A19, MATRIX_0:def 7 ;

:: thesis: verum

end;then A28: Line (B,j) = (width B) |-> (0. K) by A4;

Line (A,j) = (width A) |-> (0. K) by A4, A27;

hence (A * X) * (j,k) = ((width A) |-> (0. K)) "*" (Col (X,k)) by A10, A13, A18, MATRIX_3:def 4

.= Sum ((0. K) * (Col (X,k))) by A10, A13, FVSUM_1:66

.= (0. K) * (Sum (Col (X,k))) by FVSUM_1:73

.= 0. K

.= (Line (B,j)) . k by A11, A8, A14, A19, A28, FINSEQ_2:57

.= B * (j,k) by A11, A8, A14, A19, MATRIX_0:def 7 ;

:: thesis: verum

then A * X = B by A11, A7, A14, A16, FINSEQ_1:57, MATRIX_0:21;

hence x in Solutions_of (A,B) by A9, A10, A11, A13, A8; :: thesis: verum

hence Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B)))))) by A5; :: thesis: verum