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