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 @ ) = width A by Def7;
A2: ( len A = n & ( for p being FinSequence of K st p in rng A holds
len p = n ) ) by Def3;

A3: now

A4: n >= 0 by NAT_1:2;

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

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

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

end;

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

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

end;

end;

end;

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 )
assume A5: p in rng (A @ ) ; :: thesis: len p = n
consider n2 being Nat such that
A6: for x being set st x in rng (A @ ) holds
ex s being FinSequence st
( s = x & len s = n2 ) by Def1;
A7: 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 consider s being FinSequence such that
A8: ( s = p2 & len s = n2 ) by A6;
thus len p2 = n2 by A8; :: thesis: verum

end;

consider s being FinSequence such that
A9: ( s = p & len s = n2 ) by A5, A6;

now

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

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

then A11: width A = n by A2, Th20;
then A12: ( len (A @ ) = width A & width (A @ ) = len A ) by A10, Lm1;
then A @ is Matrix of n,n2,K by A7, A11, Def3;
hence len p = n by A2, A9, A10, A11, A12, Th20; :: thesis: verum

end;

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

then A13: width A = 0 by A2, Def4;
A14: len (A @ ) = width A by Def7;
consider x0 being set such that
A15: ( x0 in dom (A @ ) & p = (A @ ) . x0 ) by A5, FUNCT_1:def 5;
thus len p = n by A13, A14, A15, FINSEQ_1:4, FINSEQ_1:def 3; :: thesis: verum

end;

end;

end;

hence len p = n ; :: thesis: verum

end;

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