let c, m, n be Nat; :: thesis: for D being non empty set
for pD being FinSequence of D
for A being Matrix of n,m,D
for A9 being Matrix of m,n,D st A9 = A @ & ( m = 0 implies n = 0 ) holds
ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @

let D be non empty set ; :: thesis: for pD being FinSequence of D
for A being Matrix of n,m,D
for A9 being Matrix of m,n,D st A9 = A @ & ( m = 0 implies n = 0 ) holds
ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @

let pD be FinSequence of D; :: thesis: for A being Matrix of n,m,D
for A9 being Matrix of m,n,D st A9 = A @ & ( m = 0 implies n = 0 ) holds
ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @

let A be Matrix of n,m,D; :: thesis: for A9 being Matrix of m,n,D st A9 = A @ & ( m = 0 implies n = 0 ) holds
ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @

let A9 be Matrix of m,n,D; :: thesis: ( A9 = A @ & ( m = 0 implies n = 0 ) implies ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @ )
assume that
A1: A9 = A @ and
A2: ( m = 0 implies n = 0 ) ; :: thesis: ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @
set RC = ReplaceCol (A,c,pD);
set RL = ReplaceLine (A9,c,pD);
now :: thesis: ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @
per cases ( n = 0 or ( len pD <> len A & n > 0 ) or ( len pD = len A & n > 0 ) ) ;
suppose A3: n = 0 ; :: thesis: ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @
then 0 = len A by MATRIX_0:def 2;
then 0 = width A by MATRIX_0:def 3
.= len A9 by ;
then m = 0 by MATRIX_0:def 2;
then len (ReplaceLine (A9,c,pD)) = 0 by MATRIX_0:def 2;
then width (ReplaceLine (A9,c,pD)) = 0 by MATRIX_0:def 3;
then len ((ReplaceLine (A9,c,pD)) @) = 0 by MATRIX_0:def 6;
then A4: (ReplaceLine (A9,c,pD)) @ = {} ;
len (ReplaceCol (A,c,pD)) = 0 by ;
hence ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @ by A4; :: thesis: verum
end;
suppose A5: ( len pD <> len A & n > 0 ) ; :: thesis: ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @
then A6: width A = m by MATRIX_0:23;
then A7: width A9 = len A by ;
A8: len A = n by ;
thus ReplaceCol (A,c,pD) = A by
.= (A @) @ by
.= (ReplaceLine (A9,c,pD)) @ by ; :: thesis: verum
end;
suppose A9: ( len pD = len A & n > 0 ) ; :: thesis: ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @
then A10: width (ReplaceLine (A9,c,pD)) = n by ;
then A11: len ((ReplaceLine (A9,c,pD)) @) = n by ;
len (ReplaceLine (A9,c,pD)) = m by ;
then width ((ReplaceLine (A9,c,pD)) @) = m by ;
then reconsider RL9 = (ReplaceLine (A9,c,pD)) @ as Matrix of n,m,D by ;
A12: len A = n by ;
A13: width A9 = n by ;
now :: thesis: for i, j being Nat st [i,j] in Indices (ReplaceCol (A,c,pD)) holds
(ReplaceCol (A,c,pD)) * (i,j) = RL9 * (i,j)
A14: Indices (ReplaceCol (A,c,pD)) = Indices A by MATRIX_0:26;
A15: Indices (ReplaceLine (A9,c,pD)) = Indices A9 by MATRIX_0:26;
let i, j be Nat; :: thesis: ( [i,j] in Indices (ReplaceCol (A,c,pD)) implies (ReplaceCol (A,c,pD)) * (b1,b2) = RL9 * (b1,b2) )
assume A16: [i,j] in Indices (ReplaceCol (A,c,pD)) ; :: thesis: (ReplaceCol (A,c,pD)) * (b1,b2) = RL9 * (b1,b2)
reconsider I = i, J = j as Element of NAT by ORDINAL1:def 12;
Indices (ReplaceCol (A,c,pD)) = Indices RL9 by MATRIX_0:26;
then A17: [j,i] in Indices (ReplaceLine (A9,c,pD)) by ;
per cases ( J = c or J <> c ) ;
suppose A18: J = c ; :: thesis: (ReplaceCol (A,c,pD)) * (b1,b2) = RL9 * (b1,b2)
hence (ReplaceCol (A,c,pD)) * (i,j) = pD . I by A9, A16, A14, Def2
.= (ReplaceLine (A9,c,pD)) * (J,I) by
.= RL9 * (i,j) by ;
:: thesis: verum
end;
suppose A19: J <> c ; :: thesis: (ReplaceCol (A,c,pD)) * (b1,b2) = RL9 * (b1,b2)
hence (ReplaceCol (A,c,pD)) * (i,j) = A * (I,J) by A9, A16, A14, Def2
.= A9 * (j,i) by
.= (ReplaceLine (A9,c,pD)) * (J,I) by
.= RL9 * (i,j) by ;
:: thesis: verum
end;
end;
end;
hence ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @ by MATRIX_0:27; :: thesis: verum
end;
end;
end;
hence ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @ ; :: thesis: verum