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_1:def 3;
then width (Segm (A @ ),mt,nt) = 0 by A3, MATRIX_1:24, MATRIX_1:def 4;
then A4: len ((Segm (A @ ),mt,nt) @ ) = 0 by MATRIX_1:def 7;
len (Segm A,nt,mt) = 0 by A3, MATRIX_1:def 3;
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_2:15;
hence Segm A,nt,mt = (Segm (A @ ),mt,nt) @ by A1, A2, A5, Th18; :: thesis: verum

end;

end;