let D be non empty set ; 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; 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; 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; 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; ( 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
; 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; verum