let n be Nat; :: thesis: for L being non empty 1-sorted holds n -tuples_on (n -tuples_on the carrier of L) is n,L -matrix-membered
let L be non empty 1-sorted ; :: thesis: n -tuples_on (n -tuples_on the carrier of L) is n,L -matrix-membered
for X being object st X in n -tuples_on (n -tuples_on the carrier of L) holds
X is Matrix of n,L

proof

let X be object ; :: thesis: ( X in n -tuples_on (n -tuples_on the carrier of L) implies X is Matrix of n,L )
assume X in n -tuples_on (n -tuples_on the carrier of L) ; :: thesis: X is Matrix of n,L
then reconsider X = X as Element of n -tuples_on (n -tuples_on the carrier of L) ;
A1: len X = n by CARD_1:def 7;
ex m being Nat st
for y being object st y in rng X holds
ex q being FinSequence of L st
( y = q & len q = m )

proof

take n ; :: thesis: for y being object st y in rng X holds
ex q being FinSequence of L st
( y = q & len q = n )
let y be object ; :: thesis: ( y in rng X implies ex q being FinSequence of L st
( y = q & len q = n ) )
assume y in rng X ; :: thesis: ex q being FinSequence of L st
( y = q & len q = n )
then reconsider q = y as Element of n -tuples_on the carrier of L ;
reconsider q = q as FinSequence of L ;
take q ; :: thesis: ( y = q & len q = n )
thus ( y = q & len q = n ) by CARD_1:def 7; :: thesis: verum

end;

then reconsider X = X as Matrix of the carrier of L by MATRIX_0:9;
for q being FinSequence of L st q in rng X holds
len q = n

proof

let q be FinSequence of L; :: thesis: ( q in rng X implies len q = n )
A2: rng X c= n -tuples_on the carrier of L by FINSEQ_1:def 4;
assume q in rng X ; :: thesis: len q = n
then reconsider q = q as Element of n -tuples_on the carrier of L by A2;
len q = n by CARD_1:def 7;
hence len q = n ; :: thesis: verum

end;

hence X is Matrix of n,L by A1, MATRIX_0:def 2; :: thesis: verum

end;

hence n -tuples_on (n -tuples_on the carrier of L) is n,L -matrix-membered ; :: thesis: verum