let n, m 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_1:def 3;
then the_rank_of (Segm M,nt,mt) <= 0 by Th74;
hence the_rank_of (Segm M,nt,mt) = 0 ; :: thesis: verum