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

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

hence
ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @
; :: thesis: verumper cases
( n = 0 or ( len pD <> len A & n > 0 ) or ( len pD = len A & n > 0 ) )
;

end;

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 A1, MATRIX_0:def 6 ;

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 A3, MATRIX_0:def 2;

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

end;then 0 = width A by MATRIX_0:def 3

.= len A9 by A1, MATRIX_0:def 6 ;

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 A3, MATRIX_0:def 2;

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

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 A1, A2, A5, MATRIX_0:54;

A8: len A = n by A5, MATRIX_0:23;

thus ReplaceCol (A,c,pD) = A by A5, Def2

.= (A @) @ by A2, A5, A8, A6, MATRIX_0:57

.= (ReplaceLine (A9,c,pD)) @ by A1, A5, A7, MATRIX11:def 3 ; :: thesis: verum

end;then A7: width A9 = len A by A1, A2, A5, MATRIX_0:54;

A8: len A = n by A5, MATRIX_0:23;

thus ReplaceCol (A,c,pD) = A by A5, Def2

.= (A @) @ by A2, A5, A8, A6, MATRIX_0:57

.= (ReplaceLine (A9,c,pD)) @ by A1, A5, A7, MATRIX11:def 3 ; :: thesis: verum

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_0:23;

then A11: len ((ReplaceLine (A9,c,pD)) @) = n by A9, MATRIX_0:54;

len (ReplaceLine (A9,c,pD)) = m by A2, A9, MATRIX_0:23;

then width ((ReplaceLine (A9,c,pD)) @) = m by A9, A10, MATRIX_0:54;

then reconsider RL9 = (ReplaceLine (A9,c,pD)) @ as Matrix of n,m,D by A11, MATRIX_0:51;

A12: len A = n by A9, MATRIX_0:23;

A13: width A9 = n by A2, A9, MATRIX_0:23;

end;then A11: len ((ReplaceLine (A9,c,pD)) @) = n by A9, MATRIX_0:54;

len (ReplaceLine (A9,c,pD)) = m by A2, A9, MATRIX_0:23;

then width ((ReplaceLine (A9,c,pD)) @) = m by A9, A10, MATRIX_0:54;

then reconsider RL9 = (ReplaceLine (A9,c,pD)) @ as Matrix of n,m,D by A11, MATRIX_0:51;

A12: len A = n by A9, MATRIX_0:23;

A13: width A9 = n by A2, A9, MATRIX_0:23;

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)

hence
ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @
by MATRIX_0:27; :: thesis: verum(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)) * (b_{1},b_{2}) = RL9 * (b_{1},b_{2}) )

assume A16: [i,j] in Indices (ReplaceCol (A,c,pD)) ; :: thesis: (ReplaceCol (A,c,pD)) * (b_{1},b_{2}) = RL9 * (b_{1},b_{2})

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 A16, MATRIX_0:def 6;

end;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)) * (b

assume A16: [i,j] in Indices (ReplaceCol (A,c,pD)) ; :: thesis: (ReplaceCol (A,c,pD)) * (b

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 A16, MATRIX_0:def 6;

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

end;

suppose A18:
J = c
; :: thesis: (ReplaceCol (A,c,pD)) * (b_{1},b_{2}) = RL9 * (b_{1},b_{2})

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_0:def 6 ;

:: thesis: verum

end;.= (ReplaceLine (A9,c,pD)) * (J,I) by A9, A12, A13, A17, A15, A18, MATRIX11:def 3

.= RL9 * (i,j) by A17, MATRIX_0:def 6 ;

:: thesis: verum

suppose A19:
J <> c
; :: thesis: (ReplaceCol (A,c,pD)) * (b_{1},b_{2}) = RL9 * (b_{1},b_{2})

hence (ReplaceCol (A,c,pD)) * (i,j) =
A * (I,J)
by A9, A16, A14, Def2

.= A9 * (j,i) by A1, A16, A14, MATRIX_0:def 6

.= (ReplaceLine (A9,c,pD)) * (J,I) by A9, A12, A13, A17, A15, A19, MATRIX11:def 3

.= RL9 * (i,j) by A17, MATRIX_0:def 6 ;

:: thesis: verum

end;.= A9 * (j,i) by A1, A16, A14, MATRIX_0:def 6

.= (ReplaceLine (A9,c,pD)) * (J,I) by A9, A12, A13, A17, A15, A19, MATRIX11:def 3

.= RL9 * (i,j) by A17, MATRIX_0:def 6 ;

:: thesis: verum