let X, Y be non empty set ; :: thesis: for n, m being Element of NAT st n <> 0 & n -tuples_on X = m -tuples_on Y holds
( X = Y & n = m )
let n, m be Element of NAT ; :: thesis: ( n <> 0 & n -tuples_on X = m -tuples_on Y implies ( X = Y & n = m ) )
assume A1: ( n <> 0 & n -tuples_on X = m -tuples_on Y ) ; :: thesis: ( X = Y & n = m )
then A2: Seg n <> {} ;
thus X = Y :: thesis: n = m

proof

thus X c= Y :: according to XBOOLE_0:def 10 :: thesis: Y c= X

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in X or a in Y )
assume a in X ; :: thesis: a in Y
then n |-> a is Element of n -tuples_on X by FINSEQ_2:132;
then n |-> a in m -tuples_on Y by A1;
then n |-> a in { s where s is Element of Y * : len s = m } by FINSEQ_2:def 4;
then consider s being Element of Y * such that
A3: ( s = n |-> a & len s = m ) ;
A4: rng (n |-> a) c= Y by A3, FINSEQ_1:def 4;
n |-> a = (Seg n) --> a by FINSEQ_2:def 2;
then rng (n |-> a) = {a} by A2, FUNCOP_1:14;
then a in rng (n |-> a) by TARSKI:def 1;
hence a in Y by A4; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Y or a in X )
assume a in Y ; :: thesis: a in X
then m |-> a is Element of m -tuples_on Y by FINSEQ_2:132;
then m |-> a in n -tuples_on X by A1;
then m |-> a in { s where s is Element of X * : len s = n } by FINSEQ_2:def 4;
then consider s being Element of X * such that
A5: ( s = m |-> a & len s = n ) ;
A6: m = n by A5, FINSEQ_1:def 18;
A7: rng (m |-> a) c= X by A5, FINSEQ_1:def 4;
m |-> a = (Seg m) --> a by FINSEQ_2:def 2;
then rng (m |-> a) = {a} by A2, A6, FUNCOP_1:14;
then a in rng (m |-> a) by TARSKI:def 1;
hence a in X by A7; :: thesis: verum

end;

hence n = m by A1, FINSEQ_2:130; :: thesis: verum