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 [:(rng nt),(rng mt):] c= Indices A & ( m = 0 implies n = 0 ) holds
Segm (A,nt,mt) = (Segm ((A @),mt,nt)) @
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 [:(rng nt),(rng mt):] c= Indices A & ( m = 0 implies n = 0 ) holds
Segm (A,nt,mt) = (Segm ((A @),mt,nt)) @
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 [:(rng nt),(rng mt):] c= Indices A & ( m = 0 implies n = 0 ) holds
Segm (A,nt,mt) = (Segm ((A @),mt,nt)) @
let nt be Element of n -tuples_on NAT; for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A & ( m = 0 implies n = 0 ) holds
Segm (A,nt,mt) = (Segm ((A @),mt,nt)) @
let mt be Element of m -tuples_on NAT; ( [:(rng nt),(rng mt):] c= Indices A & ( m = 0 implies n = 0 ) implies Segm (A,nt,mt) = (Segm ((A @),mt,nt)) @ )
assume that
A1:
[:(rng nt),(rng mt):] c= Indices A
and
A2:
( m = 0 implies n = 0 )
; Segm (A,nt,mt) = (Segm ((A @),mt,nt)) @
set S9 = Segm ((A @),mt,nt);
set S = Segm (A,nt,mt);
per cases
( n = 0 or n > 0 )
;
suppose A3:
n = 0
;
Segm (A,nt,mt) = (Segm ((A @),mt,nt)) @
(
len (Segm ((A @),mt,nt)) = 0 or (
len (Segm ((A @),mt,nt)) > 0 &
len (Segm ((A @),mt,nt)) = m ) )
by MATRIX_0:def 2;
then
width (Segm ((A @),mt,nt)) = 0
by A3, MATRIX_0:23, MATRIX_0:def 3;
then A4:
len ((Segm ((A @),mt,nt)) @) = 0
by MATRIX_0:def 6;
len (Segm (A,nt,mt)) = 0
by A3, MATRIX_0:def 2;
then
Segm (
A,
nt,
mt)
= {}
;
hence
Segm (
A,
nt,
mt)
= (Segm ((A @),mt,nt)) @
by A4;
verum end; suppose A5:
n > 0
;
Segm (A,nt,mt) = (Segm ((A @),mt,nt)) @ then A6:
width (Segm (A,nt,mt)) = m
by Th1;
len (Segm (A,nt,mt)) = n
by A5, Th1;
then
((Segm (A,nt,mt)) @) @ = Segm (
A,
nt,
mt)
by A2, A5, A6, MATRIX_0:57;
hence
Segm (
A,
nt,
mt)
= (Segm ((A @),mt,nt)) @
by A1, A2, A5, Th18;
verum end; end;