let n be Nat; :: thesis: for L being non empty doubleLoopStr
for S being 1-sorted holds
( the carrier of S c= n -Matrices_over L iff S is n,L -matrix-membered )
let L be non empty doubleLoopStr ; :: thesis: for S being 1-sorted holds
( the carrier of S c= n -Matrices_over L iff S is n,L -matrix-membered )
let S be 1-sorted ; :: thesis: ( the carrier of S c= n -Matrices_over L iff S is n,L -matrix-membered )

hereby :: thesis: ( S is n,L -matrix-membered implies the carrier of S c= n -Matrices_over L )

assume the carrier of S c= n -Matrices_over L ; :: thesis: S is n,L -matrix-membered
then the carrier of S is n,L -matrix-membered by MATRIX_1:2;
hence S is n,L -matrix-membered ; :: thesis: verum

end;

assume A1: S is n,L -matrix-membered ; :: thesis: the carrier of S c= n -Matrices_over L
for x being object st x in the carrier of S holds
x in n -Matrices_over L

proof

let x be object ; :: thesis: ( x in the carrier of S implies x in n -Matrices_over L )
assume x in the carrier of S ; :: thesis: x in n -Matrices_over L
then x is Matrix of n,L by A1, Def3;
then x is Element of n -Matrices_over L by MATRIX_1:2;
hence x in n -Matrices_over L ; :: thesis: verum

end;

hence the carrier of S c= n -Matrices_over L by TARSKI:def 3; :: thesis: verum