let n be Element of NAT ; :: thesis: for K being non empty set
for A being Matrix of n,K holds A @ is Matrix of n,K
let K be non empty set ; :: thesis: for A being Matrix of n,K holds A @ is Matrix of n,K
let A be Matrix of n,K; :: thesis: A @ is Matrix of n,K
A1: len A = n by Def3;
A2: for p being FinSequence of K st p in rng (A @) holds
len p = n

proof

let p be FinSequence of K; :: thesis: ( p in rng (A @) implies len p = n )
consider n2 being Nat such that
A3: for x being set st x in rng (A @) holds
ex s being FinSequence st
( s = x & len s = n2 ) by Def1;
A4: for p2 being FinSequence of K st p2 in rng (A @) holds
len p2 = n2

proof

let p2 be FinSequence of K; :: thesis: ( p2 in rng (A @) implies len p2 = n2 )
assume p2 in rng (A @) ; :: thesis: len p2 = n2
then ex s being FinSequence st
( s = p2 & len s = n2 ) by A3;
hence len p2 = n2 ; :: thesis: verum

end;

assume A5: p in rng (A @) ; :: thesis: len p = n
then A6: ex s being FinSequence st
( s = p & len s = n2 ) by A3;

now

per cases ( n > 0 or n <= 0 ) ;

case A7: n > 0 ; :: thesis: len p = n

then A8: width A = n by A1, Th20;
then A9: width (A @) = len A by A7, Lm1;
A10: len (A @) = width A by A7, A8, Lm1;
then A @ is Matrix of n,n2,K by A4, A8, Def3;
hence len p = n by A1, A6, A7, A8, A10, A9, Th20; :: thesis: verum

end;

case A11: n <= 0 ; :: thesis: len p = n

A12: ( len (A @) = width A & ex x0 being set st
( x0 in dom (A @) & p = (A @) . x0 ) ) by A5, Def7, FUNCT_1:def 5;
width A = 0 by A1, A11, Def4;
then Seg (width A) = {} ;
hence len p = n by A12, FINSEQ_1:def 3; :: thesis: verum

end;

end;

end;

hence len p = n ; :: thesis: verum

end;

A13: len (A @) = width A by Def7;

now

A14: n >= 0 by NAT_1:2;

per cases ( n > 0 or n = 0 ) by A14, XXREAL_0:1;

case n > 0 ; :: thesis: len (A @) = n

hence len (A @) = n by A13, A1, Th20; :: thesis: verum

end;

case n = 0 ; :: thesis: len (A @) = n

hence len (A @) = n by A13, A1, Def4; :: thesis: verum

end;

end;

end;

hence A @ is Matrix of n,K by A2, Def3; :: thesis: verum