let D be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( [:(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 ) ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum
end;
suppose A5: n > 0 ; :: thesis: 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; :: thesis: verum
end;
end;