let D be non empty set ; for m, n being Nat holds
( [:(n -tuples_on D),(m -tuples_on D):],(n + m) -tuples_on D are_equipotent & card [:(n -tuples_on D),(m -tuples_on D):] = card ((n + m) -tuples_on D) )
let m, n be Nat; ( [:(n -tuples_on D),(m -tuples_on D):],(n + m) -tuples_on D are_equipotent & card [:(n -tuples_on D),(m -tuples_on D):] = card ((n + m) -tuples_on D) )
defpred S1[ object , object ] means ex p being Element of n -tuples_on D ex q being Element of m -tuples_on D st
( $1 = [p,q] & $2 = p ^ q );
set A = [:(n -tuples_on D),(m -tuples_on D):];
set B = (n + m) -tuples_on D;
A1:
for x being object st x in [:(n -tuples_on D),(m -tuples_on D):] holds
ex y being object st S1[x,y]
consider f being Function such that
A3:
( dom f = [:(n -tuples_on D),(m -tuples_on D):] & ( for x being object st x in [:(n -tuples_on D),(m -tuples_on D):] holds
S1[x,f . x] ) )
from CLASSES1:sch 1(A1);
thus
[:(n -tuples_on D),(m -tuples_on D):],(n + m) -tuples_on D are_equipotent
card [:(n -tuples_on D),(m -tuples_on D):] = card ((n + m) -tuples_on D)proof
take
f
;
WELLORD2:def 4 ( f is one-to-one & dom f = [:(n -tuples_on D),(m -tuples_on D):] & rng f = (n + m) -tuples_on D )
thus
f is
one-to-one
( dom f = [:(n -tuples_on D),(m -tuples_on D):] & rng f = (n + m) -tuples_on D )proof
let x,
y be
object ;
FUNCT_1:def 4 ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume
x in dom f
;
( not y in dom f or not f . x = f . y or x = y )
then consider p1 being
Element of
n -tuples_on D,
q1 being
Element of
m -tuples_on D such that A4:
x = [p1,q1]
and A5:
f . x = p1 ^ q1
by A3;
assume
y in dom f
;
( not f . x = f . y or x = y )
then consider p2 being
Element of
n -tuples_on D,
q2 being
Element of
m -tuples_on D such that A6:
y = [p2,q2]
and A7:
f . y = p2 ^ q2
by A3;
assume A8:
f . x = f . y
;
x = y
A9:
(
len p1 = n &
len p2 = n )
by CARD_1:def 7;
then consider p being
FinSequence such that A10:
p1 ^ p = p2
by A5, A7, A8, FINSEQ_1:47;
consider q being
FinSequence such that A11:
p2 ^ q = p1
by A5, A7, A8, A9, FINSEQ_1:47;
(len p1) + 0 =
(len (p1 ^ p)) + (len q)
by A10, A11, FINSEQ_1:22
.=
((len p1) + (len p)) + (len q)
by FINSEQ_1:22
.=
(len p1) + ((len p) + (len q))
;
then
p = {}
;
then
p1 = p2
by A10, FINSEQ_1:34;
hence
x = y
by A4, A5, A6, A7, A8, FINSEQ_1:33;
verum
end;
thus
dom f = [:(n -tuples_on D),(m -tuples_on D):]
by A3;
rng f = (n + m) -tuples_on D
thus
rng f c= (n + m) -tuples_on D
XBOOLE_0:def 10 (n + m) -tuples_on D c= rng f
let x be
object ;
TARSKI:def 3 ( not x in (n + m) -tuples_on D or x in rng f )
assume
x in (n + m) -tuples_on D
;
x in rng f
then reconsider x =
x as
Element of
(n + m) -tuples_on D ;
consider p being
Element of
n -tuples_on D,
q being
Element of
m -tuples_on D such that A13:
x = p ^ q
by FINSEQ_2:106;
consider p1 being
Element of
n -tuples_on D,
q1 being
Element of
m -tuples_on D such that A14:
[p,q] = [p1,q1]
and A15:
f . [p,q] = p1 ^ q1
by A3;
(
p1 = p &
q1 = q )
by A14, XTUPLE_0:1;
hence
x in rng f
by A3, A13, A15, FUNCT_1:def 3;
verum
end;
hence
card [:(n -tuples_on D),(m -tuples_on D):] = card ((n + m) -tuples_on D)
by CARD_1:5; verum