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))*>*> )
A1: 1 in Seg 1 ;
assume that
A2: n = 1 and
A3: m = 1 ; :: thesis: Segm A,nt,mt = <*<*(A * (nt . 1),(mt . 1))*>*>
Indices (Segm A,nt,mt) = [:(Seg 1),(Seg 1):] by A2, A3, MATRIX_1:25;
then [1,1] in Indices (Segm A,nt,mt) by A1, 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 A2, A3, Th20; :: thesis: verum