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 & n > 0 holds

Solutions_of (A,B) c= 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 & n > 0 holds

Solutions_of (A,B) c= 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 & n > 0 holds

Solutions_of (A,B) c= 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 & n > 0 implies Solutions_of (A,B) c= 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: n > 0 ; :: thesis: Solutions_of (A,B) c= Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B))))))

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

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

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

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

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

A5: len (Segm (B,nt,(Sgm (Seg (width B))))) = n by A2, MATRIX_0:23;

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

then A6: 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 (A,B) or x in Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B)))))) )

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

consider X being Matrix of K such that

A8: x = X and

A9: len X = width A and

A10: width X = width B and

A11: A * X = B by A7;

set SX = (Segm (A,nt,(Sgm (Seg (width A))))) * X;

A12: len A = len B by A7, Th33;

then (Segm (A,nt,(Sgm (Seg (width A))))) * X = Segm (B,nt,(Sgm (Seg (width B)))) by A10, A3, A5, A6, A13, MATRIX_0:21;

hence x in Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B)))))) by A8, A9, A10, A4, A6; :: thesis: verum

for A, B being Matrix of K

for nt being Element of n -tuples_on NAT st rng nt c= dom A & n > 0 holds

Solutions_of (A,B) c= 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 & n > 0 holds

Solutions_of (A,B) c= 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 & n > 0 holds

Solutions_of (A,B) c= 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 & n > 0 implies Solutions_of (A,B) c= 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: n > 0 ; :: thesis: Solutions_of (A,B) c= Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B))))))

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

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

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

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

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

A5: len (Segm (B,nt,(Sgm (Seg (width B))))) = n by A2, MATRIX_0:23;

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

then A6: 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 (A,B) or x in Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B)))))) )

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

consider X being Matrix of K such that

A8: x = X and

A9: len X = width A and

A10: width X = width B and

A11: A * X = B by A7;

set SX = (Segm (A,nt,(Sgm (Seg (width A))))) * X;

A12: len A = len B by A7, Th33;

A13: now :: thesis: for j, k being Nat st [j,k] in Indices ((Segm (A,nt,(Sgm (Seg (width A))))) * X) holds

((Segm (A,nt,(Sgm (Seg (width A))))) * X) * (j,k) = (Segm (B,nt,(Sgm (Seg (width B))))) * (j,k)

( len ((Segm (A,nt,(Sgm (Seg (width A))))) * X) = len (Segm (A,nt,(Sgm (Seg (width A))))) & width ((Segm (A,nt,(Sgm (Seg (width A))))) * X) = width X )
by A9, A4, MATRIX_3:def 4;((Segm (A,nt,(Sgm (Seg (width A))))) * X) * (j,k) = (Segm (B,nt,(Sgm (Seg (width B))))) * (j,k)

A14:
len ((Segm (A,nt,(Sgm (Seg (width A))))) * X) = len (Segm (A,nt,(Sgm (Seg (width A)))))
by A9, A4, MATRIX_3:def 4;

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

assume A15: [j,k] in Indices ((Segm (A,nt,(Sgm (Seg (width A))))) * X) ; :: thesis: ((Segm (A,nt,(Sgm (Seg (width A))))) * X) * (j,k) = (Segm (B,nt,(Sgm (Seg (width B))))) * (j,k)

j in dom ((Segm (A,nt,(Sgm (Seg (width A))))) * X) by A15, ZFMISC_1:87;

then A16: j in Seg n by A3, A14, FINSEQ_1:def 3;

width ((Segm (A,nt,(Sgm (Seg (width A))))) * X) = width X by A9, A4, MATRIX_3:def 4;

then A17: k in Seg (width B) by A10, A15, ZFMISC_1:87;

dom nt = Seg n by FINSEQ_2:124;

then nt . j in rng nt by A16, FUNCT_1:def 3;

then A18: nt . j in dom A by A1;

dom A = Seg (len B) by A12, FINSEQ_1:def 3;

then nt . j in dom B by A18, FINSEQ_1:def 3;

then A19: [(nt . j),k] in Indices B by A17, ZFMISC_1:87;

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

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

then A20: (Sgm (Seg (width B))) . k9 = k by A17, FINSEQ_2:49;

j in dom (Segm (B,nt,(Sgm (Seg (width B))))) by A5, A16, FINSEQ_1:def 3;

then A21: [j,k] in Indices (Segm (B,nt,(Sgm (Seg (width B))))) by A6, A17, ZFMISC_1:87;

Line ((Segm (A,nt,(Sgm (Seg (width A))))),j) = Line (A,(nt . j)) by A16, Lm6;

hence ((Segm (A,nt,(Sgm (Seg (width A))))) * X) * (j,k) = (Line (A,(nt . j))) "*" (Col (X,k)) by A9, A4, A15, MATRIX_3:def 4

.= B * ((nt . j9),k) by A9, A11, A19, MATRIX_3:def 4

.= (Segm (B,nt,(Sgm (Seg (width B))))) * (j,k) by A21, A20, MATRIX13:def 1 ;

:: thesis: verum

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

assume A15: [j,k] in Indices ((Segm (A,nt,(Sgm (Seg (width A))))) * X) ; :: thesis: ((Segm (A,nt,(Sgm (Seg (width A))))) * X) * (j,k) = (Segm (B,nt,(Sgm (Seg (width B))))) * (j,k)

j in dom ((Segm (A,nt,(Sgm (Seg (width A))))) * X) by A15, ZFMISC_1:87;

then A16: j in Seg n by A3, A14, FINSEQ_1:def 3;

width ((Segm (A,nt,(Sgm (Seg (width A))))) * X) = width X by A9, A4, MATRIX_3:def 4;

then A17: k in Seg (width B) by A10, A15, ZFMISC_1:87;

dom nt = Seg n by FINSEQ_2:124;

then nt . j in rng nt by A16, FUNCT_1:def 3;

then A18: nt . j in dom A by A1;

dom A = Seg (len B) by A12, FINSEQ_1:def 3;

then nt . j in dom B by A18, FINSEQ_1:def 3;

then A19: [(nt . j),k] in Indices B by A17, ZFMISC_1:87;

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

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

then A20: (Sgm (Seg (width B))) . k9 = k by A17, FINSEQ_2:49;

j in dom (Segm (B,nt,(Sgm (Seg (width B))))) by A5, A16, FINSEQ_1:def 3;

then A21: [j,k] in Indices (Segm (B,nt,(Sgm (Seg (width B))))) by A6, A17, ZFMISC_1:87;

Line ((Segm (A,nt,(Sgm (Seg (width A))))),j) = Line (A,(nt . j)) by A16, Lm6;

hence ((Segm (A,nt,(Sgm (Seg (width A))))) * X) * (j,k) = (Line (A,(nt . j))) "*" (Col (X,k)) by A9, A4, A15, MATRIX_3:def 4

.= B * ((nt . j9),k) by A9, A11, A19, MATRIX_3:def 4

.= (Segm (B,nt,(Sgm (Seg (width B))))) * (j,k) by A21, A20, MATRIX13:def 1 ;

:: thesis: verum

then (Segm (A,nt,(Sgm (Seg (width A))))) * X = Segm (B,nt,(Sgm (Seg (width B)))) by A10, A3, A5, A6, A13, MATRIX_0:21;

hence x in Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B)))))) by A8, A9, A10, A4, A6; :: thesis: verum