let X, Y be non empty non-empty FinSequence; :: thesis: ex I being Function of [:(product X),(product Y):],(product (X ^ Y)) st
( I is one-to-one & I is onto & ( for x, y being FinSequence st x in product X & y in product Y holds
I . (x,y) = x ^ y ) )
defpred S1[ set , set , set ] means ex x, y being FinSequence st
( x = $1 & y = $2 & $3 = x ^ y );
P1: for x, y being set st x in product X & y in product Y holds
ex z being set st
( z in product (X ^ Y) & S1[x,y,z] )
proof
let x, y be set ; :: thesis: ( x in product X & y in product Y implies ex z being set st
( z in product (X ^ Y) & S1[x,y,z] ) )
assume AS0: ( x in product X & y in product Y ) ; :: thesis: ex z being set st
( z in product (X ^ Y) & S1[x,y,z] )
then consider g being Function such that
Z01: ( x = g & dom g = dom X & ( for z being set st z in dom X holds
g . z in X . z ) ) by CARD_3:def 5;
Z02: dom g = Seg (len X) by Z01, FINSEQ_1:def 3;
then reconsider g = g as FinSequence by FINSEQ_1:def 2;
consider h being Function such that
Z04: ( y = h & dom h = dom Y & ( for z being set st z in dom Y holds
h . z in Y . z ) ) by CARD_3:def 5, AS0;
Z05: dom h = Seg (len Y) by Z04, FINSEQ_1:def 3;
then reconsider h = h as FinSequence by FINSEQ_1:def 2;
Z03: ( len g = len X & len h = len Y ) by FINSEQ_1:def 3, Z02, Z05;
Z07: dom (g ^ h) = Seg ((len g) + (len h)) by FINSEQ_1:def 7
.= Seg (len (X ^ Y)) by Z03, FINSEQ_1:35
.= dom (X ^ Y) by FINSEQ_1:def 3 ;
for z being set st z in dom (X ^ Y) holds
(g ^ h) . z in (X ^ Y) . z
proof
let z be set ; :: thesis: ( z in dom (X ^ Y) implies (g ^ h) . z in (X ^ Y) . z )
assume Z081: z in dom (X ^ Y) ; :: thesis: (g ^ h) . z in (X ^ Y) . z
then reconsider k = z as Element of NAT ;
per cases ( k in dom X or ex n being Nat st
( n in dom Y & k = (len X) + n ) ) by FINSEQ_1:38, Z081;
suppose C1: k in dom X ; :: thesis: (g ^ h) . z in (X ^ Y) . z
then C11: g . k in X . k by Z01;
g . k = (g ^ h) . k by C1, Z01, FINSEQ_1:def 7;
hence (g ^ h) . z in (X ^ Y) . z by C11, C1, FINSEQ_1:def 7; :: thesis: verum
end;
suppose ex n being Nat st
( n in dom Y & k = (len X) + n ) ; :: thesis: (g ^ h) . z in (X ^ Y) . z
then consider n being Nat such that
C21: ( n in dom Y & k = (len X) + n ) ;
C11: h . n in Y . n by C21, Z04;
h . n = (g ^ h) . k by C21, Z03, Z04, FINSEQ_1:def 7;
hence (g ^ h) . z in (X ^ Y) . z by C11, C21, FINSEQ_1:def 7; :: thesis: verum
end;
end;
end;
then g ^ h in product (X ^ Y) by Z07, CARD_3:18;
hence ex z being set st
( z in product (X ^ Y) & S1[x,y,z] ) by Z01, Z04; :: thesis: verum
end;
consider I being Function of [:(product X),(product Y):],(product (X ^ Y)) such that
P2: for x, y being set st x in product X & y in product Y holds
S1[x,y,I . (x,y)] from BINOP_1:sch 1(P1);
 P2X: for x, y being FinSequence st x in product X & y in product Y holds
I . (x,y) = x ^ y
proof
let x, y be FinSequence; :: thesis: ( x in product X & y in product Y implies I . (x,y) = x ^ y )
assume ( x in product X & y in product Y ) ; :: thesis: I . (x,y) = x ^ y
then ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) by P2;
hence I . (x,y) = x ^ y ; :: thesis: verum
end;
now
let z1, z2 be set ; :: thesis: ( z1 in [:(product X),(product Y):] & z2 in [:(product X),(product Y):] & I . z1 = I . z2 implies z1 = z2 )
assume P3: ( z1 in [:(product X),(product Y):] & z2 in [:(product X),(product Y):] & I . z1 = I . z2 ) ; :: thesis: z1 = z2
consider x1, y1 being set such that
P4: ( x1 in product X & y1 in product Y & z1 = [x1,y1] ) by ZFMISC_1:def 2, P3;
consider x2, y2 being set such that
P5: ( x2 in product X & y2 in product Y & z2 = [x2,y2] ) by ZFMISC_1:def 2, P3;
consider xx1, yy1 being FinSequence such that
P60: ( xx1 = x1 & yy1 = y1 & I . (x1,y1) = xx1 ^ yy1 ) by P2, P4;
consider xx2, yy2 being FinSequence such that
P61: ( xx2 = x2 & yy2 = y2 & I . (x2,y2) = xx2 ^ yy2 ) by P2, P5;
P81: dom xx1 = dom X by P4, P60, CARD_3:18
.= dom xx2 by P5, P61, CARD_3:18 ;
xx1 = (xx1 ^ yy1) | (dom xx1) by FINSEQ_1:33
.= xx2 by P3, P4, P5, P60, P61, P81, FINSEQ_1:33 ;
hence z1 = z2 by P3, P4, P5, P60, P61, FINSEQ_1:46; :: thesis: verum
end;
then P3: I is one-to-one by FUNCT_2:25;
now
let w be set ; :: thesis: ( w in product (X ^ Y) implies w in rng I )
assume w in product (X ^ Y) ; :: thesis: w in rng I
then consider g being Function such that
X1: ( w = g & dom g = dom (X ^ Y) & ( for i being set st i in dom (X ^ Y) holds
g . i in (X ^ Y) . i ) ) by CARD_3:def 5;
X2: dom g = Seg (len (X ^ Y)) by X1, FINSEQ_1:def 3;
then reconsider g = g as FinSequence by FINSEQ_1:def 2;
set x = g | (len X);
set y = g /^ (len X);
A1: g is FinSequence of rng g by FINSEQ_1:def 4;
rng g <> {} by X1, RELAT_1:65;
then A3: (g | (len X)) ^ (g /^ (len X)) = g by RFINSEQ:21, A1;
XX3: len (X ^ Y) = (len X) + (len Y) by FINSEQ_1:35;
then XX4: len X <= len (X ^ Y) by NAT_1:11;
XX2: len g = len (X ^ Y) by FINSEQ_1:def 3, X2;
then len (g | (len X)) = len X by XX3, NAT_1:11, FINSEQ_1:80;
then Z07: dom (g | (len X)) = Seg (len X) by FINSEQ_1:def 3
.= dom X by FINSEQ_1:def 3 ;
for z being set st z in dom X holds
(g | (len X)) . z in X . z
proof
let z be set ; :: thesis: ( z in dom X implies (g | (len X)) . z in X . z )
assume C1: z in dom X ; :: thesis: (g | (len X)) . z in X . z
then reconsider k = z as Element of NAT ;
C2: dom X c= dom (X ^ Y) by FINSEQ_1:39;
C12: (g | (len X)) . k = g . k by C1, A3, Z07, FINSEQ_1:def 7;
X . k = (X ^ Y) . k by C1, FINSEQ_1:def 7;
hence (g | (len X)) . z in X . z by C12, X1, C1, C2; :: thesis: verum
end;
then A4: g | (len X) in product X by Z07, CARD_3:18;
dom (g | (len X)) = Seg (len X) by Z07, FINSEQ_1:def 3;
then A41: len (g | (len X)) = len X by FINSEQ_1:def 3;
len (g /^ (len X)) = (len g) - (len X) by XX4, XX2, RFINSEQ:def 2
.= len Y by XX2, XX3 ;
then Seg (len (g /^ (len X))) = dom Y by FINSEQ_1:def 3;
then Z09: dom (g /^ (len X)) = dom Y by FINSEQ_1:def 3;
for z being set st z in dom Y holds
(g /^ (len X)) . z in Y . z
proof
let z be set ; :: thesis: ( z in dom Y implies (g /^ (len X)) . z in Y . z )
assume C1: z in dom Y ; :: thesis: (g /^ (len X)) . z in Y . z
then reconsider k = z as Element of NAT ;
C12: (g /^ (len X)) . k = g . ((len X) + k) by C1, A3, A41, Z09, FINSEQ_1:def 7;
Y . k = (X ^ Y) . ((len X) + k) by C1, FINSEQ_1:def 7;
hence (g /^ (len X)) . z in Y . z by C12, X1, FINSEQ_1:41, C1; :: thesis: verum
end;
then A5: g /^ (len X) in product Y by Z09, CARD_3:18;
reconsider z = [(g | (len X)),(g /^ (len X))] as Element of [:(product X),(product Y):] by A4, A5, ZFMISC_1:106;
w = I . ((g | (len X)),(g /^ (len X))) by X1, A3, P2X, A4, A5
.= I . z ;
hence w in rng I by FUNCT_2:189; :: thesis: verum
end;
then product (X ^ Y) c= rng I by TARSKI:def 3;
then product (X ^ Y) = rng I by XBOOLE_0:def 10;
then I is onto by FUNCT_2:def 3;
hence ex I being Function of [:(product X),(product Y):],(product (X ^ Y)) st
( I is one-to-one & I is onto & ( for x, y being FinSequence st x in product X & y in product Y holds
I . (x,y) = x ^ y ) ) by P2X, P3; :: thesis: verum