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 = 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 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 = 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_0:24;
A4: 2 in Seg 2 ;
then [2,2] in Indices (Segm (A,nt,mt)) by A3, ZFMISC_1:87;
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:87;
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:87;
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:87;
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