let D be non empty set ; :: thesis: for n, m being Element of 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 n, m be Element of NAT ; :: thesis: ( [:(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[ set , set ] 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;
A4:
for x being set st x in [:(n -tuples_on D),(m -tuples_on D):] holds
ex y being set st S1[x,y]
proof
let x be
set ;
:: thesis: ( x in [:(n -tuples_on D),(m -tuples_on D):] implies ex y being set st S1[x,y] )
assume A5:
x in [:(n -tuples_on D),(m -tuples_on D):]
;
:: thesis: ex y being set st S1[x,y]
then A6:
(
x = [(x `1 ),(x `2 )] &
x `1 in n -tuples_on D &
x `2 in m -tuples_on D )
by MCART_1:10, MCART_1:23;
reconsider p =
x `1 as
Element of
n -tuples_on D by A5, MCART_1:10;
reconsider q =
x `2 as
Element of
m -tuples_on D by A5, MCART_1:10;
reconsider y =
p ^ q as
set ;
take
y
;
:: thesis: S1[x,y]
thus
S1[
x,
y]
by A6;
:: thesis: verum
end;
consider f being Function such that
A7:
( dom f = [:(n -tuples_on D),(m -tuples_on D):] & ( for x being set st x in [:(n -tuples_on D),(m -tuples_on D):] holds
S1[x,f . x] ) )
from CLASSES1:sch 1(A4);
thus
[:(n -tuples_on D),(m -tuples_on D):],(n + m) -tuples_on D are_equipotent
:: thesis: card [:(n -tuples_on D),(m -tuples_on D):] = card ((n + m) -tuples_on D)proof
take
f
;
:: according to WELLORD2:def 4 :: thesis: ( 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
:: thesis: ( dom f = [:(n -tuples_on D),(m -tuples_on D):] & rng f = (n + m) -tuples_on D )proof
let x be
set ;
:: according to FUNCT_1:def 8 :: thesis: for b1 being set holds
( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 )let y be
set ;
:: thesis: ( 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
;
:: thesis: ( 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 A8:
(
x = [p1,q1] &
f . x = p1 ^ q1 )
by A7;
assume
y in dom f
;
:: thesis: ( 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 A9:
(
y = [p2,q2] &
f . y = p2 ^ q2 )
by A7;
assume A10:
f . x = f . y
;
:: thesis: x = y
then A11:
(
p1 ^ q1 = p2 ^ q2 &
len p1 = n &
len p2 = n &
len q1 = m &
len q2 = m )
by A8, A9, FINSEQ_1:def 18;
then consider p being
FinSequence such that A12:
p1 ^ p = p2
by FINSEQ_1:64;
consider q being
FinSequence such that A13:
p2 ^ q = p1
by A11, FINSEQ_1:64;
(len p1) + 0 =
(len (p1 ^ p)) + (len q)
by A12, A13, FINSEQ_1:35
.=
((len p1) + (len p)) + (len q)
by FINSEQ_1:35
.=
(len p1) + ((len p) + (len q))
;
then
p = {}
;
then
p1 = p2
by A12, FINSEQ_1:47;
hence
x = y
by A8, A9, A10, FINSEQ_1:46;
:: thesis: verum
end;
thus
dom f = [:(n -tuples_on D),(m -tuples_on D):]
by A7;
:: thesis: rng f = (n + m) -tuples_on D
thus
rng f c= (n + m) -tuples_on D
:: according to XBOOLE_0:def 10 :: thesis: (n + m) -tuples_on D c= rng f
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in (n + m) -tuples_on D or x in rng f )
assume
x in (n + m) -tuples_on D
;
:: thesis: 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 A15:
x = p ^ q
by FINSEQ_2:126;
consider p1 being
Element of
n -tuples_on D,
q1 being
Element of
m -tuples_on D such that A16:
(
[p,q] = [p1,q1] &
f . [p,q] = p1 ^ q1 )
by A7;
(
p1 = p &
q1 = q )
by A16, ZFMISC_1:33;
hence
x in rng f
by A7, A15, A16, FUNCT_1:def 5;
:: thesis: verum
end;
hence
card [:(n -tuples_on D),(m -tuples_on D):] = card ((n + m) -tuples_on D)
by CARD_1:21; :: thesis: verum