let D, E be non empty set ; :: thesis: ( D c= E implies for X being Matrix of D holds X is Matrix of E )
assume A1: D c= E ; :: thesis: for X being Matrix of D holds X is Matrix of E
let X be Matrix of D; :: thesis: X is Matrix of E
D * c= E * by A1, FINSEQ_1:62;
then rng X c= E * by XBOOLE_1:1;
hence X is Matrix of E by FINSEQ_1:def 4; :: thesis: verum