let D be non empty set ; :: thesis: for n, m 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 n = 1 & m = 1 holds
Segm A,nt,mt = <*<*(A * (nt . 1),(mt . 1))*>*>
let n, m 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 n = 1 & m = 1 holds
Segm A,nt,mt = <*<*(A * (nt . 1),(mt . 1))*>*>
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 n = 1 & m = 1 holds
Segm A,nt,mt = <*<*(A * (nt . 1),(mt . 1))*>*>
let nt be Element of n -tuples_on NAT ; :: thesis: for mt being Element of m -tuples_on NAT st n = 1 & m = 1 holds
Segm A,nt,mt = <*<*(A * (nt . 1),(mt . 1))*>*>
let mt be Element of m -tuples_on NAT ; :: thesis: ( n = 1 & m = 1 implies Segm A,nt,mt = <*<*(A * (nt . 1),(mt . 1))*>*> )
assume A1: ( n = 1 & m = 1 ) ; :: thesis: Segm A,nt,mt = <*<*(A * (nt . 1),(mt . 1))*>*>
then ( 1 in Seg 1 & Indices (Segm A,nt,mt) = [:(Seg 1),(Seg 1):] ) by MATRIX_1:25;
then [1,1] in Indices (Segm A,nt,mt) by ZFMISC_1:106;
then (Segm A,nt,mt) * 1,1 = A * (nt . 1),(mt . 1) by Def1;
hence Segm A,nt,mt = <*<*(A * (nt . 1),(mt . 1))*>*> by A1, Th20; :: thesis: verum