let m, n be Nat; :: thesis: for D, E being non empty set st D c= E holds
for X being Matrix of m,n,D holds X is Matrix of m,n,E
let D, E be non empty set ; :: thesis: ( D c= E implies for X being Matrix of m,n,D holds X is Matrix of m,n,E )
assume A1: D c= E ; :: thesis: for X being Matrix of m,n,D holds X is Matrix of m,n,E
let X be Matrix of m,n,D; :: thesis: X is Matrix of m,n,E
reconsider x = X as Matrix of E by A1, Th80;
( len x = m & ( for p being FinSequence of E st p in rng x holds
len p = n ) )

proof

thus len x = m by MATRIX_0:def 2; :: thesis: for p being FinSequence of E st p in rng x holds
len p = n
let p be FinSequence of E; :: thesis: ( p in rng x implies len p = n )
assume A2: p in rng x ; :: thesis: len p = n
then p in rng X ;
then reconsider p9 = p as FinSequence of D by FINSEQ_1:def 11;
p9 in rng X by A2;
hence len p = n by MATRIX_0:def 2; :: thesis: verum

end;

hence X is Matrix of m,n,E by MATRIX_0:def 2; :: thesis: verum