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 that
A1: n = 2 and
A2: 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))
A3: Indices (Segm A,nt,mt) = [:(Seg 2),(Seg 2):] by A1, A2, MATRIX_1:25;
A4: 2 in Seg 2 ;
then [2,2] in Indices (Segm A,nt,mt) by A3, ZFMISC_1:106;
then A5: (Segm A,nt,mt) * 2,2 = A * (nt . 2),(mt . 2) by Def1;
A6: 1 in Seg 2 ;
then [1,1] in Indices (Segm A,nt,mt) by A3, ZFMISC_1:106;
then A7: (Segm A,nt,mt) * 1,1 = A * (nt . 1),(mt . 1) by Def1;
[2,1] in Indices (Segm A,nt,mt) by A6, A4, A3, ZFMISC_1:106;
then A8: (Segm A,nt,mt) * 2,1 = A * (nt . 2),(mt . 1) by Def1;
[1,2] in Indices (Segm A,nt,mt) by A6, A4, A3, ZFMISC_1:106;
then (Segm A,nt,mt) * 1,2 = A * (nt . 1),(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, A2, A7, A8, A5, Th22; :: thesis: verum