let D be non empty set ; for M being Matrix of D st len M > 0 & width M > 0 holds
(M @) @ = M
let M be Matrix of D; ( len M > 0 & width M > 0 implies (M @) @ = M )
assume that
A1:
len M > 0
and
A2:
width M > 0
; (M @) @ = M
set N = M @ ;
A3:
width (M @) = len M
by A2, Th54;
A4:
len ((M @) @) = width (M @)
by Def6;
A5:
len (M @) = width M
by Def6;
( dom M = Seg (len M) & dom ((M @) @) = Seg (len ((M @) @)) )
by FINSEQ_1:def 3;
then A6:
Indices ((M @) @) = Indices M
by A1, A5, A3, A4, Th54;
A7:
for i, j being Nat st [i,j] in Indices ((M @) @) holds
((M @) @) * (i,j) = M * (i,j)
proof
let i,
j be
Nat;
( [i,j] in Indices ((M @) @) implies ((M @) @) * (i,j) = M * (i,j) )
assume A8:
[i,j] in Indices ((M @) @)
;
((M @) @) * (i,j) = M * (i,j)
then
[j,i] in Indices (M @)
by Def6;
then
((M @) @) * (
i,
j)
= (M @) * (
j,
i)
by Def6;
hence
((M @) @) * (
i,
j)
= M * (
i,
j)
by A6, A8, Def6;
verum
end;
width (M @) > 0
by A1, A2, Th54;
then
width ((M @) @) = width M
by A5, Th54;
hence
(M @) @ = M
by A3, A4, A7, Th21; verum