let D1, D2 be set ; :: thesis: ( D1 c= D2 implies D1 * c= D2 * )
assume A1: D1 c= D2 ; :: thesis: D1 * c= D2 *
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D1 * or x in D2 * )
assume x in D1 * ; :: thesis: x in D2 *
then reconsider p = x as FinSequence of D1 by Def11;
rng p c= D1 by Def4;
then x is FinSequence of D2 by Def4, A1, XBOOLE_1:1;
hence x in D2 * by Def11; :: thesis: verum