let D, E be non empty set ; for M being Matrix of D
for L being Matrix of E st M = L holds
M @ = L @
let M be Matrix of D; for L being Matrix of E st M = L holds
M @ = L @
let L be Matrix of E; ( M = L implies M @ = L @ )
assume AS:
M = L
; M @ = L @
for i, j being Nat st [i,j] in Indices (M @) holds
(M @) * (i,j) in E
proof
let i,
j be
Nat;
( [i,j] in Indices (M @) implies (M @) * (i,j) in E )
assume
[i,j] in Indices (M @)
;
(M @) * (i,j) in E
then A2:
[j,i] in Indices M
by MATRIX_0:def 6;
then (M @) * (
i,
j) =
M * (
j,
i)
by MATRIX_0:def 6
.=
L * (
j,
i)
by AS, A2, EQ2
;
hence
(M @) * (
i,
j)
in E
;
verum
end;
then reconsider M1 = M @ as Matrix of E by REALTOINT;
P1:
len M1 = width L
by AS, MATRIX_0:def 6;
P2:
for i, j being Nat holds
( [i,j] in Indices M1 iff [j,i] in Indices L )
by AS, MATRIX_0:def 6;
for i, j being Nat st [j,i] in Indices L holds
M1 * (i,j) = L * (j,i)
proof
let i,
j be
Nat;
( [j,i] in Indices L implies M1 * (i,j) = L * (j,i) )
assume A2:
[j,i] in Indices L
;
M1 * (i,j) = L * (j,i)
then
[i,j] in Indices (M @)
by AS, MATRIX_0:def 6;
then M1 * (
i,
j) =
(M @) * (
i,
j)
by EQ2
.=
M * (
j,
i)
by AS, A2, MATRIX_0:def 6
;
hence
M1 * (
i,
j)
= L * (
j,
i)
by AS, A2, EQ2;
verum
end;
hence
M @ = L @
by P1, P2, MATRIX_0:def 6; verum