let c, m, n be Nat; for D being non empty set
for AD being Matrix of n,m,D holds RCol (AD,c,(Col (AD,c))) = AD
let D be non empty set ; for AD being Matrix of n,m,D holds RCol (AD,c,(Col (AD,c))) = AD
let AD be Matrix of n,m,D; RCol (AD,c,(Col (AD,c))) = AD
set C = Col (AD,c);
set R = RCol (AD,c,(Col (AD,c)));
now for i, j being Nat st [i,j] in Indices AD holds
(RCol (AD,c,(Col (AD,c)))) * (i,j) = AD * (i,j)reconsider c =
c as
Element of
NAT by ORDINAL1:def 12;
let i,
j be
Nat;
( [i,j] in Indices AD implies (RCol (AD,c,(Col (AD,c)))) * (i,j) = AD * (i,j) )assume A1:
[i,j] in Indices AD
;
(RCol (AD,c,(Col (AD,c)))) * (i,j) = AD * (i,j)A2:
len (Col (AD,c)) = len AD
by MATRIX_0:def 8;
reconsider I =
i,
J =
j as
Element of
NAT by ORDINAL1:def 12;
A3:
i in dom AD
by A1, ZFMISC_1:87;
now (RCol (AD,c,(Col (AD,c)))) * (i,j) = AD * (i,j)per cases
( c = j or c <> J )
;
suppose A4:
c = j
;
(RCol (AD,c,(Col (AD,c)))) * (i,j) = AD * (i,j)hence (RCol (AD,c,(Col (AD,c)))) * (
i,
j) =
(Col (AD,c)) . I
by A1, A2, Def2
.=
AD * (
i,
j)
by A3, A4, MATRIX_0:def 8
;
verum end; end; end; hence
(RCol (AD,c,(Col (AD,c)))) * (
i,
j)
= AD * (
i,
j)
;
verum end;
hence
RCol (AD,c,(Col (AD,c))) = AD
by MATRIX_0:27; verum