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 ())))),(Segm (B,nt,(Sgm (Seg ())))))

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 ())))),(Segm (B,nt,(Sgm (Seg ())))))

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 ())))),(Segm (B,nt,(Sgm (Seg ())))))

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 ())))),(Segm (B,nt,(Sgm (Seg ()))))) )
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 ())))),(Segm (B,nt,(Sgm (Seg ())))))
set SA = Segm (A,nt,(Sgm (Seg ())));
A3: len (Segm (A,nt,(Sgm (Seg ())))) = n by ;
width (Segm (A,nt,(Sgm (Seg ())))) = card (Seg ()) by ;
then A4: width (Segm (A,nt,(Sgm (Seg ())))) = width A by FINSEQ_1:57;
set SB = Segm (B,nt,(Sgm (Seg ())));
A5: len (Segm (B,nt,(Sgm (Seg ())))) = n by ;
width (Segm (B,nt,(Sgm (Seg ())))) = card (Seg ()) by ;
then A6: width (Segm (B,nt,(Sgm (Seg ())))) = 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 ())))),(Segm (B,nt,(Sgm (Seg ()))))) )
assume A7: x in Solutions_of (A,B) ; :: thesis: x in Solutions_of ((Segm (A,nt,(Sgm (Seg ())))),(Segm (B,nt,(Sgm (Seg ())))))
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 ())))) * X;
A12: len A = len B by ;
A13: now :: thesis: for j, k being Nat st [j,k] in Indices ((Segm (A,nt,(Sgm (Seg ())))) * X) holds
((Segm (A,nt,(Sgm (Seg ())))) * X) * (j,k) = (Segm (B,nt,(Sgm (Seg ())))) * (j,k)
A14: len ((Segm (A,nt,(Sgm (Seg ())))) * X) = len (Segm (A,nt,(Sgm (Seg ())))) by ;
let j, k be Nat; :: thesis: ( [j,k] in Indices ((Segm (A,nt,(Sgm (Seg ())))) * X) implies ((Segm (A,nt,(Sgm (Seg ())))) * X) * (j,k) = (Segm (B,nt,(Sgm (Seg ())))) * (j,k) )
assume A15: [j,k] in Indices ((Segm (A,nt,(Sgm (Seg ())))) * X) ; :: thesis: ((Segm (A,nt,(Sgm (Seg ())))) * X) * (j,k) = (Segm (B,nt,(Sgm (Seg ())))) * (j,k)
j in dom ((Segm (A,nt,(Sgm (Seg ())))) * X) by ;
then A16: j in Seg n by ;
width ((Segm (A,nt,(Sgm (Seg ())))) * X) = width X by ;
then A17: k in Seg () by ;
dom nt = Seg n by FINSEQ_2:124;
then nt . j in rng nt by ;
then A18: nt . j in dom A by A1;
dom A = Seg (len B) by ;
then nt . j in dom B by ;
then A19: [(nt . j),k] in Indices B by ;
reconsider j9 = j, k9 = k as Element of NAT by ORDINAL1:def 12;
Sgm (Seg ()) = idseq () by FINSEQ_3:48;
then A20: (Sgm (Seg ())) . k9 = k by ;
j in dom (Segm (B,nt,(Sgm (Seg ())))) by ;
then A21: [j,k] in Indices (Segm (B,nt,(Sgm (Seg ())))) by ;
Line ((Segm (A,nt,(Sgm (Seg ())))),j) = Line (A,(nt . j)) by ;
hence ((Segm (A,nt,(Sgm (Seg ())))) * X) * (j,k) = (Line (A,(nt . j))) "*" (Col (X,k)) by
.= B * ((nt . j9),k) by
.= (Segm (B,nt,(Sgm (Seg ())))) * (j,k) by ;
:: thesis: verum
end;
( len ((Segm (A,nt,(Sgm (Seg ())))) * X) = len (Segm (A,nt,(Sgm (Seg ())))) & width ((Segm (A,nt,(Sgm (Seg ())))) * X) = width X ) by ;
then (Segm (A,nt,(Sgm (Seg ())))) * X = Segm (B,nt,(Sgm (Seg ()))) by ;
hence x in Solutions_of ((Segm (A,nt,(Sgm (Seg ())))),(Segm (B,nt,(Sgm (Seg ()))))) by A8, A9, A10, A4, A6; :: thesis: verum