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 XBOOLE_1:26, Lm8;
then A1: ((m -tuples_on A) /\ (m -tuples_on A)) /\ (B *) c= (m -tuples_on A) /\ (m -tuples_on B) by XBOOLE_1:16;
now :: thesis: for x being object st x in m -tuples_on B holds
x in B *
let x be object ; :: thesis: ( x in m -tuples_on B implies x in B * )
assume A2: 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 A2;
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 A) /\ (m -tuples_on B) c= (m -tuples_on A) /\ (B *) by XBOOLE_1:26, TARSKI:def 3;
hence (m -tuples_on A) /\ (B *) = (m -tuples_on A) /\ (m -tuples_on B) by A1; :: thesis: verum