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;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (m -tuples_on A) /\ (B *) or x in m -tuples_on B )
assume x in (m -tuples_on A) /\ (B *) ; :: thesis: x in m -tuples_on B
then A1: ( x in m -tuples_on A & x in B * ) by XBOOLE_0:def 4;
then A2: ( x is m -element FinSequence & x is FinSequence of B ) by FINSEQ_2:141, FINSEQ_1:def 11;
reconsider xx = x as FinSequence of B by A1, FINSEQ_1:def 11;
len xx = m by A2, 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 Lm7; :: thesis: verum