let c, m, n be Nat; :: thesis: 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 ; :: thesis: for AD being Matrix of n,m,D holds RCol (AD,c,(Col (AD,c))) = AD

let AD be Matrix of n,m,D; :: thesis: RCol (AD,c,(Col (AD,c))) = AD

set C = Col (AD,c);

set R = RCol (AD,c,(Col (AD,c)));

for AD being Matrix of n,m,D holds RCol (AD,c,(Col (AD,c))) = AD

let D be non empty set ; :: thesis: for AD being Matrix of n,m,D holds RCol (AD,c,(Col (AD,c))) = AD

let AD be Matrix of n,m,D; :: thesis: RCol (AD,c,(Col (AD,c))) = AD

set C = Col (AD,c);

set R = RCol (AD,c,(Col (AD,c)));

now :: thesis: for i, j being Nat st [i,j] in Indices AD holds

(RCol (AD,c,(Col (AD,c)))) * (i,j) = AD * (i,j)

hence
RCol (AD,c,(Col (AD,c))) = AD
by MATRIX_0:27; :: thesis: verum(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; :: thesis: ( [i,j] in Indices AD implies (RCol (AD,c,(Col (AD,c)))) * (i,j) = AD * (i,j) )

assume A1: [i,j] in Indices AD ; :: thesis: (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;

end;let i, j be Nat; :: thesis: ( [i,j] in Indices AD implies (RCol (AD,c,(Col (AD,c)))) * (i,j) = AD * (i,j) )

assume A1: [i,j] in Indices AD ; :: thesis: (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 :: thesis: (RCol (AD,c,(Col (AD,c)))) * (i,j) = AD * (i,j)

hence
(RCol (AD,c,(Col (AD,c)))) * (i,j) = AD * (i,j)
; :: thesis: verumend;