let D be non empty set ; :: thesis: for m, n, i, j being Element of NAT
for A being Matrix of m,n,D holds Swap A,i,j is Matrix of m,n,D
let m, n, i, j be Element of NAT ; :: thesis: for A being Matrix of m,n,D holds Swap A,i,j is Matrix of m,n,D
let A be Matrix of m,n,D; :: thesis: Swap A,i,j is Matrix of m,n,D
rng (Swap A,i,j) = rng A by FINSEQ_7:24;
then ex n3 being Nat st
for x being set st x in rng (Swap A,i,j) holds
ex p being FinSequence of D st
( x = p & len p = n3 ) by MATRIX_1:9;
then A7: Swap A,i,j is Matrix of D by MATRIX_1:9;
A2: ( len A = m & ( for p being FinSequence of D st p in rng A holds
len p = n ) ) by MATRIX_1:def 3;
A3: for p being FinSequence of D st p in rng (Swap A,i,j) holds
len p = n

proof

let p be FinSequence of D; :: thesis: ( p in rng (Swap A,i,j) implies len p = n )
assume B1: p in rng (Swap A,i,j) ; :: thesis: len p = n
rng (Swap A,i,j) = rng A by FINSEQ_7:24;
hence len p = n by B1, MATRIX_1:def 3; :: thesis: verum

end;

len (Swap A,i,j) = len A by FINSEQ_7:20;
hence Swap A,i,j is Matrix of m,n,D by A2, A3, A7, MATRIX_1:def 3; :: thesis: verum