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

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_1:def 3;
then 0 = width A by MATRIX_1:def 4
.= len A9 by A1, MATRIX_1:def 7 ;
then m = 0 by MATRIX_1:def 3;
then len (ReplaceLine A9,c,pD) = 0 by MATRIX_1:def 3;
then width (ReplaceLine A9,c,pD) = 0 by MATRIX_1:def 4;
then len ((ReplaceLine A9,c,pD) @ ) = 0 by MATRIX_1:def 7;
then A4: (ReplaceLine A9,c,pD) @ = {} ;
len (ReplaceCol A,c,pD) = 0 by A3, MATRIX_1:def 3;
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_1:24;
then A7: width A9 = len A by A1, A2, A5, MATRIX_2:12;
A8: len A = n by A5, MATRIX_1:24;
thus ReplaceCol A,c,pD = A by A5, Def2
.= (A @ ) @ by A2, A5, A8, A6, MATRIX_2:15
.= (ReplaceLine A9,c,pD) @ by A1, A5, A7, MATRIX11:def 3 ; :: 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 A2, MATRIX_1:24;
then A11: len ((ReplaceLine A9,c,pD) @ ) = n by A9, MATRIX_2:12;
len (ReplaceLine A9,c,pD) = m by A2, A9, MATRIX_1:24;
then width ((ReplaceLine A9,c,pD) @ ) = m by A9, A10, MATRIX_2:12;
then reconsider RL9 = (ReplaceLine A9,c,pD) @ as Matrix of n,m,D by A11, MATRIX_2:7;
A12: len A = n by A9, MATRIX_1:24;
A13: width A9 = n by A2, A9, MATRIX_1:24;

now

A14: Indices (ReplaceCol A,c,pD) = Indices A by MATRIX_1:27;
A15: Indices (ReplaceLine A9,c,pD) = Indices A9 by MATRIX_1:27;
let i, j be Nat; :: thesis: ( [i,j] in Indices (ReplaceCol A,c,pD) implies (ReplaceCol A,c,pD) * b₁,b₂ = RL9 * b₁,b₂ )
assume A16: [i,j] in Indices (ReplaceCol A,c,pD) ; :: thesis: (ReplaceCol A,c,pD) * b₁,b₂ = RL9 * b₁,b₂
reconsider I = i, J = j as Element of NAT by ORDINAL1:def 13;
Indices (ReplaceCol A,c,pD) = Indices RL9 by MATRIX_1:27;
then A17: [j,i] in Indices (ReplaceLine A9,c,pD) by A16, MATRIX_1:def 7;

per cases ( J = c or J <> c ) ;

suppose A18: J = c ; :: thesis: (ReplaceCol A,c,pD) * b₁,b₂ = RL9 * b₁,b₂

hence (ReplaceCol A,c,pD) * i,j = pD . I by A9, A16, A14, Def2
.= (ReplaceLine A9,c,pD) * J,I by A9, A12, A13, A17, A15, A18, MATRIX11:def 3
.= RL9 * i,j by A17, MATRIX_1:def 7 ;
:: thesis: verum

end;

suppose A19: J <> c ; :: thesis: (ReplaceCol A,c,pD) * b₁,b₂ = RL9 * b₁,b₂

hence (ReplaceCol A,c,pD) * i,j = A * I,J by A9, A16, A14, Def2
.= A9 * j,i by A1, A16, A14, MATRIX_1:def 7
.= (ReplaceLine A9,c,pD) * J,I by A9, A12, A13, A17, A15, A19, MATRIX11:def 3
.= RL9 * i,j by A17, MATRIX_1:def 7 ;
:: thesis: verum

end;

end;

end;

hence ReplaceCol A,c,pD = (ReplaceLine A9,c,pD) @ by MATRIX_1:28; :: thesis: verum

end;

end;

end;

hence ReplaceCol A,c,pD = (ReplaceLine A9,c,pD) @ ; :: thesis: verum