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 )

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

hence x is Element of n -Matrices_over K by A4, FINSEQ_2:92; :: thesis: verum

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 Matrix of n,K
; :: thesis: x is Element of n -Matrices_over K
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 )

for q being FinSequence of K st q in rng x holds

len q = n

end;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

then reconsider x = x as Matrix of the carrier of K by MATRIX_0:9;
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;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

for q being FinSequence of K st q in rng x holds

len q = n

proof

hence
x is Matrix of n,K
by A1, MATRIX_0:def 2; :: thesis: verum
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;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

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

then
x is FinSequence of n -tuples_on the carrier of K
by FINSEQ_1:def 4;
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;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

hence x is Element of n -Matrices_over K by A4, FINSEQ_2:92; :: thesis: verum