A1: F is FinSequence of n -tuples_on the carrier of K by Th102;
now :: thesis: for x being object st x in rng F holds
ex p being FinSequence of K st
( x = p & len p = n )
A2: rng F c= n -tuples_on the carrier of K by A1, FINSEQ_1:def 4;
let x be object ; :: thesis: ( x in rng F implies ex p being FinSequence of K st
( x = p & len p = n ) )
assume x in rng F ; :: thesis: ex p being FinSequence of K st
( x = p & len p = n )
then reconsider p = x as Element of n -tuples_on the carrier of K by A2;
len p = n by CARD_1:def 7;
hence ex p being FinSequence of K st
( x = p & len p = n ) ; :: thesis: verum
end;
then reconsider F9 = F as Matrix of K by MATRIX_0:9;
now :: thesis: for p being FinSequence of K st p in rng F9 holds
len p = n
A3: rng F9 c= n -tuples_on the carrier of K by A1, FINSEQ_1:def 4;
let p be FinSequence of K; :: thesis: ( p in rng F9 implies len p = n )
assume p in rng F9 ; :: thesis: len p = n
hence len p = n by A3, CARD_1:def 7; :: thesis: verum
end;
hence F is Matrix of len F,n,K by MATRIX_0:def 2; :: thesis: verum