let D be non empty set ; :: thesis: 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; :: 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[ 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]
proof
let x be object ; :: thesis: ( x in [:(n -tuples_on D),(m -tuples_on D):] implies ex y being object st S1[x,y] )
assume A2: x in [:(n -tuples_on D),(m -tuples_on D):] ; :: thesis: ex y being object st S1[x,y]
then reconsider p = x `1 as Element of n -tuples_on D by MCART_1:10;
reconsider q = x `2 as Element of m -tuples_on D by A2, MCART_1:10;
reconsider y = p ^ q as set ;
take y ; :: thesis: S1[x,y]
x = [(x `1),(x `2)] by A2, MCART_1:21;
hence S1[x,y] ; :: thesis: verum
end;
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 :: 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, y be object ; :: according to FUNCT_1:def 4 :: 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
A4: x = [p1,q1] and
A5: f . x = p1 ^ q1 by A3;
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
A6: y = [p2,q2] and
A7: f . y = p2 ^ q2 by A3;
assume A8: f . x = f . y ; :: thesis: 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; :: thesis: verum
end;
thus dom f = [:(n -tuples_on D),(m -tuples_on D):] by A3; :: 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
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in (n + m) -tuples_on D )
assume x in rng f ; :: thesis: x in (n + m) -tuples_on D
then consider y being object such that
A12: ( y in dom f & x = f . y ) by FUNCT_1:def 3;
ex p being Element of n -tuples_on D ex q being Element of m -tuples_on D st
( y = [p,q] & x = p ^ q ) by A3, A12;
then x is Tuple of n + m,D ;
then x is Element of (n + m) -tuples_on D by FINSEQ_2:131;
hence x in (n + m) -tuples_on D ; :: thesis: verum
end;
let x be object ; :: 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
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; :: thesis: verum
end;
hence card [:(n -tuples_on D),(m -tuples_on D):] = card ((n + m) -tuples_on D) by CARD_1:5; :: thesis: verum