let c, m, n be Nat; :: thesis: for D being non empty set

for AD being Matrix of n,m,D

for pD being FinSequence of D st not c in Seg (width AD) holds

RCol (AD,c,pD) = AD

let D be non empty set ; :: thesis: for AD being Matrix of n,m,D

for pD being FinSequence of D st not c in Seg (width AD) holds

RCol (AD,c,pD) = AD

let AD be Matrix of n,m,D; :: thesis: for pD being FinSequence of D st not c in Seg (width AD) holds

RCol (AD,c,pD) = AD

let pD be FinSequence of D; :: thesis: ( not c in Seg (width AD) implies RCol (AD,c,pD) = AD )

assume A1: not c in Seg (width AD) ; :: thesis: RCol (AD,c,pD) = AD

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

for AD being Matrix of n,m,D

for pD being FinSequence of D st not c in Seg (width AD) holds

RCol (AD,c,pD) = AD

let D be non empty set ; :: thesis: for AD being Matrix of n,m,D

for pD being FinSequence of D st not c in Seg (width AD) holds

RCol (AD,c,pD) = AD

let AD be Matrix of n,m,D; :: thesis: for pD being FinSequence of D st not c in Seg (width AD) holds

RCol (AD,c,pD) = AD

let pD be FinSequence of D; :: thesis: ( not c in Seg (width AD) implies RCol (AD,c,pD) = AD )

assume A1: not c in Seg (width AD) ; :: thesis: RCol (AD,c,pD) = AD

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

per cases
( len pD = len AD or len pD <> len AD )
;

end;

suppose A2:
len pD = len AD
; :: thesis: RCol (AD,c,pD) = AD

end;

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

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

hence
RCol (AD,c,pD) = AD
by MATRIX_0:27; :: thesis: verum(RCol (AD,c,pD)) * (i,j) = AD * (i,j)

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

assume A3: [i,j] in Indices AD ; :: thesis: (RCol (AD,c,pD)) * (i,j) = AD * (i,j)

j in Seg (width AD) by A3, ZFMISC_1:87;

hence (RCol (AD,c,pD)) * (i,j) = AD * (i,j) by A1, A2, A3, Def2; :: thesis: verum

end;assume A3: [i,j] in Indices AD ; :: thesis: (RCol (AD,c,pD)) * (i,j) = AD * (i,j)

j in Seg (width AD) by A3, ZFMISC_1:87;

hence (RCol (AD,c,pD)) * (i,j) = AD * (i,j) by A1, A2, A3, Def2; :: thesis: verum