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 ;
then consider p being object such that
A1: p in (m -tuples_on A) /\ (n -tuples_on B) ;
A2: ( p in m -tuples_on A & p in n -tuples_on B ) by XBOOLE_0:def 4, A1;
reconsider pA = p as m -element FinSequence by FINSEQ_2:141, A2;
reconsider pB = p as n -element FinSequence by FINSEQ_2:141, A2;
m = len pA by CARD_1:def 7
.= len pB
.= n by CARD_1:def 7 ;
hence m = n ; :: thesis: verum