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 n = 1 & m = 1 holds
Segm (A,nt,mt) = <*<*(A * ((nt . 1),(mt . 1)))*>*>
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 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_0:24;
then [1,1] in Indices (Segm (A,nt,mt)) by A1, ZFMISC_1:87;
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