let n, m, c 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;

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

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

now

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:106;
hence (RCol AD,c,pD) * i,j = AD * i,j by A1, A2, A3, Def2; :: thesis: verum

end;

hence RCol AD,c,pD = AD by MATRIX_1:28; :: thesis: verum

end;

suppose len pD <> len AD ; :: thesis: RCol AD,c,pD = AD

hence RCol AD,c,pD = AD by Def2; :: thesis: verum

end;

end;