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 = 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; 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; 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; 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; ( 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
; 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; verum