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 that
A1: n <> 0 and
A2: n -tuples_on X = m -tuples_on Y ; :: thesis: ( X = Y & n = m )
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 object ; :: 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:112;
then n |-> a in m -tuples_on Y by A2;
then n |-> a in { s where s is Element of Y * : len s = m } by FINSEQ_2:def 4;
then ex s being Element of Y * st
( s = n |-> a & len s = m ) ;
then A3: rng (n |-> a) c= Y by FINSEQ_1:def 4;
n |-> a = (Seg n) --> a by FINSEQ_2:def 2;
then rng (n |-> a) = {a} by A1, FUNCOP_1:8;
then a in rng (n |-> a) by TARSKI:def 1;
hence a in Y by A3; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Y or a in X )
A4: m |-> a = (Seg m) --> a by FINSEQ_2:def 2;
assume a in Y ; :: thesis: a in X
then m |-> a is Element of m -tuples_on Y by FINSEQ_2:112;
then m |-> a in n -tuples_on X by A2;
then m |-> a in { s where s is Element of X * : len s = n } by FINSEQ_2:def 4;
then A5: ex s being Element of X * st
( s = m |-> a & len s = n ) ;
then m = n by CARD_1:def 7;
then rng (m |-> a) = {a} by A1, A4, FUNCOP_1:8;
then A6: a in rng (m |-> a) by TARSKI:def 1;
rng (m |-> a) c= X by A5, FINSEQ_1:def 4;
hence a in X by A6; :: thesis: verum
end;
thus n = m by A2, FINSEQ_2:110; :: thesis: verum