let x be object ; :: thesis: for n being Nat
for K being non empty doubleLoopStr holds
( x is Element of n -Matrices_over K iff x is Matrix of n,K )
let n be Nat; :: thesis: for K being non empty doubleLoopStr holds
( x is Element of n -Matrices_over K iff x is Matrix of n,K )
let K be non empty doubleLoopStr ; :: thesis: ( x is Element of n -Matrices_over K iff x is Matrix of n,K )
thus ( x is Element of n -Matrices_over K implies x is Matrix of n,K ) :: thesis: ( x is Matrix of n,K implies x is Element of n -Matrices_over K )

proof

assume x is Element of n -Matrices_over K ; :: thesis: x is Matrix of n,K
then reconsider x = x as Element of n -tuples_on (n -tuples_on the carrier of K) ;
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 K 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 K st
( y = q & len q = n )
let y be object ; :: thesis: ( y in rng x implies ex q being FinSequence of K st
( y = q & len q = n ) )
A2: rng x c= n -tuples_on the carrier of K by FINSEQ_1:def 4;
assume y in rng x ; :: thesis: ex q being FinSequence of K st
( y = q & len q = n )
then reconsider q = y as Element of n -tuples_on the carrier of K by A2;
reconsider q = q as FinSequence of K ;
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 K by MATRIX_0:9;
for q being FinSequence of K st q in rng x holds
len q = n

proof

let q be FinSequence of K; :: thesis: ( q in rng x implies len q = n )
A3: rng x c= n -tuples_on the carrier of K 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 K by A3;
len q = n by CARD_1:def 7;
hence len q = n ; :: thesis: verum

end;

hence x is Matrix of n,K by A1, MATRIX_0:def 2; :: thesis: verum

end;

assume x is Matrix of n,K ; :: thesis: x is Element of n -Matrices_over K
then reconsider x = x as Matrix of n,K ;
A4: len x = n by MATRIX_0:def 2;
then reconsider x = x as Element of n -tuples_on ( the carrier of K *) by FINSEQ_2:92;
rng x c= n -tuples_on the carrier of K

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng x or y in n -tuples_on the carrier of K )
assume A5: y in rng x ; :: thesis: y in n -tuples_on the carrier of K
rng x c= the carrier of K * by FINSEQ_1:def 4;
then reconsider p = y as FinSequence of K by A5, FINSEQ_1:def 11;
len p = n by A5, MATRIX_0:def 2;
then p is Element of n -tuples_on the carrier of K by FINSEQ_2:92;
hence y in n -tuples_on the carrier of K ; :: thesis: verum

end;

then x is FinSequence of n -tuples_on the carrier of K by FINSEQ_1:def 4;
hence x is Element of n -Matrices_over K by A4, FINSEQ_2:92; :: thesis: verum