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
A1: 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 )
A2: rng (Swap (A,i,j)) = rng A by FINSEQ_7:22;
assume p in rng (Swap (A,i,j)) ; :: thesis: len p = n
hence len p = n by A2, MATRIX_0:def 2; :: thesis: verum

end;

rng (Swap (A,i,j)) = rng A by FINSEQ_7:22;
then ex n3 being Nat st
for x being object st x in rng (Swap (A,i,j)) holds
ex p being FinSequence of D st
( x = p & len p = n3 ) by MATRIX_0:9;
then A3: Swap (A,i,j) is Matrix of D by MATRIX_0:9;
( len A = m & len (Swap (A,i,j)) = len A ) by FINSEQ_7:18, MATRIX_0:def 2;
hence Swap (A,i,j) is Matrix of m,n,D by A3, A1, MATRIX_0:def 2; :: thesis: verum