let m, n be Nat; :: thesis: for K being Field
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for M being Matrix of K st ( n = 0 or m = 0 ) holds
the_rank_of (Segm (M,nt,mt)) = 0
let K be Field; :: thesis: for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for M being Matrix of K st ( n = 0 or m = 0 ) holds
the_rank_of (Segm (M,nt,mt)) = 0
let nt be Element of n -tuples_on NAT; :: thesis: for mt being Element of m -tuples_on NAT
for M being Matrix of K st ( n = 0 or m = 0 ) holds
the_rank_of (Segm (M,nt,mt)) = 0
let mt be Element of m -tuples_on NAT; :: thesis: for M being Matrix of K st ( n = 0 or m = 0 ) holds
the_rank_of (Segm (M,nt,mt)) = 0
let M be Matrix of K; :: thesis: ( ( n = 0 or m = 0 ) implies the_rank_of (Segm (M,nt,mt)) = 0 )
set S = Segm (M,nt,mt);
assume ( n = 0 or m = 0 ) ; :: thesis: the_rank_of (Segm (M,nt,mt)) = 0
then ( len (Segm (M,nt,mt)) = 0 or width (Segm (M,nt,mt)) = 0 ) by Th1, MATRIX_0:def 2;
hence the_rank_of (Segm (M,nt,mt)) = 0 by Th74; :: thesis: verum