let A, B be set ; :: thesis: for m, n being Nat st m -tuples_on A meets n -tuples_on B holds
m = n
let m, n be Nat; :: thesis: ( m -tuples_on A meets n -tuples_on B implies m = n )
assume m -tuples_on A meets n -tuples_on B ; :: thesis: m = n
then not (m -tuples_on A) /\ (n -tuples_on B) is empty by XBOOLE_0:def 7;
then consider p being set such that
B1: p in (m -tuples_on A) /\ (n -tuples_on B) by XBOOLE_0:def 1;
B2: ( p in m -tuples_on A & p in n -tuples_on B ) by B1, XBOOLE_0:def 4;
reconsider pA = p as m -element FinSequence by B2, FINSEQ_2:141;
reconsider pB = p as n -element FinSequence by B2, FINSEQ_2:141;
m = len pA by CARD_1:def 7
.= len pB
.= n by CARD_1:def 7 ;
hence m = n ; :: thesis: verum