let A, B be set ; :: thesis: for m being Nat holds (m -tuples_on A) /\ (B *) = (m -tuples_on A) /\ (m -tuples_on B)
let m be Nat; :: thesis: (m -tuples_on A) /\ (B *) = (m -tuples_on A) /\ (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 A) /\ (m -tuples_on B);
(m -tuples_on A) /\ ((m -tuples_on A) /\ (B *)) c= (m -tuples_on A) /\ (m -tuples_on B) by Lm11, XBOOLE_1:26;
then A2: ((m -tuples_on A) /\ (m -tuples_on A)) /\ (B *) c= (m -tuples_on A) /\ (m -tuples_on B) by XBOOLE_1:16;

now

let x be set ; :: thesis: ( x in m -tuples_on B implies x in B * )
assume C1: x in m -tuples_on B ; :: thesis: x in B *
then reconsider xx = x as m -element FinSequence by FINSEQ_2:141;
xx in mm -tuples_on B by C1;
then ( len xx = mm & rng xx c= B ) by FINSEQ_2:132;
then x is FinSequence of B by FINSEQ_1:def 4;
hence x in B * by FINSEQ_1:def 11; :: thesis: verum

end;

then m -tuples_on B c= B * by TARSKI:def 3;
then (m -tuples_on A) /\ (m -tuples_on B) c= (m -tuples_on A) /\ (B *) by XBOOLE_1:26;
hence (m -tuples_on A) /\ (B *) = (m -tuples_on A) /\ (m -tuples_on B) by A2, XBOOLE_0:def 10; :: thesis: verum