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);

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

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

now :: thesis: for i, j being Nat st [i,j] in Indices AD holds
(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;

hence RCol (AD,c,pD) = AD by MATRIX_0:27; :: 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;