let A, B be set ; :: thesis: for m being Nat holds (m -tuples_on A) /\ (B *) c= m -tuples_on B
let m be Nat; :: thesis: (m -tuples_on A) /\ (B *) c= m -tuples_on B
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
set L = (m -tuples_on A) /\ (B *);
set R = m -tuples_on B;

now

let x be set ; :: thesis: ( x in (m -tuples_on A) /\ (B *) implies x in m -tuples_on B )
assume x in (m -tuples_on A) /\ (B *) ; :: thesis: x in m -tuples_on B
then Z1: ( x in m -tuples_on A & x in B * ) by XBOOLE_0:def 4;
then B1: ( x is m -element FinSequence & x is FinSequence of B ) by FINSEQ_1:def 11, FINSEQ_2:141;
reconsider xx = x as FinSequence of B by Z1, FINSEQ_1:def 11;
len xx = m by B1, CARD_1:def 7;
then ( xx = xx & dom xx = Seg m & rng xx c= B ) by FINSEQ_1:def 3;
then xx in Funcs ((Seg m),B) by FUNCT_2:def 2;
hence x in m -tuples_on B by Lm21; :: thesis: verum

end;

hence (m -tuples_on A) /\ (B *) c= m -tuples_on B by TARSKI:def 3; :: thesis: verum