let D be non empty set ; for m, n being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st nt = idseq (len A) & mt = idseq (width A) holds
Segm (A,nt,mt) = A
let m, n be Nat; for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st nt = idseq (len A) & mt = idseq (width A) holds
Segm (A,nt,mt) = A
let A be Matrix of D; for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st nt = idseq (len A) & mt = idseq (width A) holds
Segm (A,nt,mt) = A
let nt be Element of n -tuples_on NAT; for mt being Element of m -tuples_on NAT st nt = idseq (len A) & mt = idseq (width A) holds
Segm (A,nt,mt) = A
let mt be Element of m -tuples_on NAT; ( nt = idseq (len A) & mt = idseq (width A) implies Segm (A,nt,mt) = A )
set S = Segm (A,nt,mt);
assume that
A1:
nt = idseq (len A)
and
A2:
mt = idseq (width A)
; Segm (A,nt,mt) = A
A3:
len nt = n
by CARD_1:def 7;
A4:
len (idseq (width A)) = width A
by CARD_1:def 7;
A5:
len (idseq (len A)) = len A
by CARD_1:def 7;
A6:
len mt = m
by CARD_1:def 7;
per cases
( n = 0 or n > 0 )
;
suppose A9:
n > 0
;
Segm (A,nt,mt) = Athen A10:
width (Segm (A,nt,mt)) = m
by Th1;
then A11:
Indices (Segm (A,nt,mt)) = [:(Seg n),(Seg m):]
by MATRIX_0:25;
A12:
now for i, j being Nat st [i,j] in Indices (Segm (A,nt,mt)) holds
(Segm (A,nt,mt)) * (i,j) = A * (i,j)let i,
j be
Nat;
( [i,j] in Indices (Segm (A,nt,mt)) implies (Segm (A,nt,mt)) * (i,j) = A * (i,j) )assume A13:
[i,j] in Indices (Segm (A,nt,mt))
;
(Segm (A,nt,mt)) * (i,j) = A * (i,j)reconsider i9 =
i,
j9 =
j as
Element of
NAT by ORDINAL1:def 12;
j in Seg m
by A10, A13, ZFMISC_1:87;
then A14:
mt . j9 = j
by A2, A6, A4, FINSEQ_2:49;
i in Seg n
by A11, A13, ZFMISC_1:87;
then
nt . i9 = i
by A1, A3, A5, FINSEQ_2:49;
hence
(Segm (A,nt,mt)) * (
i,
j)
= A * (
i,
j)
by A13, A14, Def1;
verum end;
len (Segm (A,nt,mt)) = n
by A9, Th1;
hence
Segm (
A,
nt,
mt)
= A
by A1, A2, A3, A6, A5, A4, A10, A12, MATRIX_0:21;
verum end; end;