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[ object , object , object ] means ex x, y being FinSequence st
( x = $1 & y = $2 & $3 = x ^ y );
A1: for x, y being object st x in product X & y in product Y holds
ex z being object st
( z in product (X ^ Y) & S1[x,y,z] )
proof
let x, y be object ; :: thesis: ( x in product X & y in product Y implies ex z being object st
( z in product (X ^ Y) & S1[x,y,z] ) )
assume A2: ( x in product X & y in product Y ) ; :: thesis: ex z being object st
( z in product (X ^ Y) & S1[x,y,z] )
then consider g being Function such that
A3: ( x = g & dom g = dom X & ( for z being object st z in dom X holds
g . z in X . z ) ) by CARD_3:def 5;
A4: dom g = Seg (len X) by A3, FINSEQ_1:def 3;
then reconsider g = g as FinSequence by FINSEQ_1:def 2;
consider h being Function such that
A5: ( y = h & dom h = dom Y & ( for z being object st z in dom Y holds
h . z in Y . z ) ) by A2, CARD_3:def 5;
A6: dom h = Seg (len Y) by A5, FINSEQ_1:def 3;
then reconsider h = h as FinSequence by FINSEQ_1:def 2;
A7: ( len g = len X & len h = len Y ) by A4, A6, FINSEQ_1:def 3;
A8: dom (g ^ h) = Seg ((len g) + (len h)) by FINSEQ_1:def 7
.= Seg (len (X ^ Y)) by A7, FINSEQ_1:22
.= dom (X ^ Y) by FINSEQ_1:def 3 ;
for z being object st z in dom (X ^ Y) holds
(g ^ h) . z in (X ^ Y) . z
proof
let z be object ; :: thesis: ( z in dom (X ^ Y) implies (g ^ h) . z in (X ^ Y) . z )
assume A9: 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 A9, FINSEQ_1:25;
suppose A10: k in dom X ; :: thesis: (g ^ h) . z in (X ^ Y) . z
then A11: g . k in X . k by A3;
g . k = (g ^ h) . k by A10, A3, FINSEQ_1:def 7;
hence (g ^ h) . z in (X ^ Y) . z by A11, A10, 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
A12: ( n in dom Y & k = (len X) + n ) ;
A13: h . n in Y . n by A12, A5;
h . n = (g ^ h) . k by A12, A7, A5, FINSEQ_1:def 7;
hence (g ^ h) . z in (X ^ Y) . z by A13, A12, FINSEQ_1:def 7; :: thesis: verum
end;
end;
end;
then g ^ h in product (X ^ Y) by A8, CARD_3:9;
hence ex z being object st
( z in product (X ^ Y) & S1[x,y,z] ) by A3, A5; :: thesis: verum
end;
consider I being Function of [:(product X),(product Y):],(product (X ^ Y)) such that
A14: for x, y being object st x in product X & y in product Y holds
S1[x,y,I . (x,y)] from BINOP_1:sch 1(A1);
 A15: 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 A14;
hence I . (x,y) = x ^ y ; :: thesis: verum
end;
now :: thesis: for z1, z2 being object st z1 in [:(product X),(product Y):] & z2 in [:(product X),(product Y):] & I . z1 = I . z2 holds
z1 = z2
let z1, z2 be object ; :: thesis: ( z1 in [:(product X),(product Y):] & z2 in [:(product X),(product Y):] & I . z1 = I . z2 implies z1 = z2 )
assume A16: ( z1 in [:(product X),(product Y):] & z2 in [:(product X),(product Y):] & I . z1 = I . z2 ) ; :: thesis: z1 = z2
consider x1, y1 being object such that
A17: ( x1 in product X & y1 in product Y & z1 = [x1,y1] ) by A16, ZFMISC_1:def 2;
consider x2, y2 being object such that
A18: ( x2 in product X & y2 in product Y & z2 = [x2,y2] ) by A16, ZFMISC_1:def 2;
consider xx1, yy1 being FinSequence such that
A19: ( xx1 = x1 & yy1 = y1 & I . (x1,y1) = xx1 ^ yy1 ) by A14, A17;
consider xx2, yy2 being FinSequence such that
A20: ( xx2 = x2 & yy2 = y2 & I . (x2,y2) = xx2 ^ yy2 ) by A14, A18;
A21: dom xx1 = dom X by A17, A19, CARD_3:9
.= dom xx2 by A18, A20, CARD_3:9 ;
xx1 = (xx1 ^ yy1) | (dom xx1) by FINSEQ_1:21
.= xx2 by A16, A17, A18, A19, A20, A21, FINSEQ_1:21 ;
hence z1 = z2 by A16, A17, A18, A19, A20, FINSEQ_1:33; :: thesis: verum
end;
then A22: I is one-to-one by FUNCT_2:19;
now :: thesis: for w being object st w in product (X ^ Y) holds
w in rng I
let w be object ; :: 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
A23: ( w = g & dom g = dom (X ^ Y) & ( for i being object st i in dom (X ^ Y) holds
g . i in (X ^ Y) . i ) ) by CARD_3:def 5;
A24: dom g = Seg (len (X ^ Y)) by A23, 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);
A26: (g | (len X)) ^ (g /^ (len X)) = g by RFINSEQ:8;
A27: len (X ^ Y) = (len X) + (len Y) by FINSEQ_1:22;
then A28: len X <= len (X ^ Y) by NAT_1:11;
A29: len g = len (X ^ Y) by A24, FINSEQ_1:def 3;
then len (g | (len X)) = len X by A27, FINSEQ_1:59, NAT_1:11;
then A30: dom (g | (len X)) = Seg (len X) by FINSEQ_1:def 3
.= dom X by FINSEQ_1:def 3 ;
for z being object st z in dom X holds
(g | (len X)) . z in X . z
proof
let z be object ; :: thesis: ( z in dom X implies (g | (len X)) . z in X . z )
assume A31: z in dom X ; :: thesis: (g | (len X)) . z in X . z
then reconsider k = z as Element of NAT ;
A32: dom X c= dom (X ^ Y) by FINSEQ_1:26;
A33: (g | (len X)) . k = g . k by A31, A26, A30, FINSEQ_1:def 7;
X . k = (X ^ Y) . k by A31, FINSEQ_1:def 7;
hence (g | (len X)) . z in X . z by A33, A23, A31, A32; :: thesis: verum
end;
then A34: g | (len X) in product X by A30, CARD_3:9;
dom (g | (len X)) = Seg (len X) by A30, FINSEQ_1:def 3;
then A35: len (g | (len X)) = len X by FINSEQ_1:def 3;
len (g /^ (len X)) = (len g) - (len X) by A28, A29, RFINSEQ:def 1
.= len Y by A29, A27 ;
then Seg (len (g /^ (len X))) = dom Y by FINSEQ_1:def 3;
then A36: dom (g /^ (len X)) = dom Y by FINSEQ_1:def 3;
for z being object st z in dom Y holds
(g /^ (len X)) . z in Y . z
proof
let z be object ; :: thesis: ( z in dom Y implies (g /^ (len X)) . z in Y . z )
assume A37: z in dom Y ; :: thesis: (g /^ (len X)) . z in Y . z
then reconsider k = z as Element of NAT ;
A38: (g /^ (len X)) . k = g . ((len X) + k) by A37, A26, A35, A36, FINSEQ_1:def 7;
Y . k = (X ^ Y) . ((len X) + k) by A37, FINSEQ_1:def 7;
hence (g /^ (len X)) . z in Y . z by A38, A23, A37, FINSEQ_1:28; :: thesis: verum
end;
then A39: g /^ (len X) in product Y by A36, CARD_3:9;
reconsider z = [(g | (len X)),(g /^ (len X))] as Element of [:(product X),(product Y):] by A34, A39, ZFMISC_1:87;
w = I . ((g | (len X)),(g /^ (len X))) by A23, A26, A15, A34, A39
.= I . z ;
hence w in rng I by FUNCT_2:112; :: 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 A15, A22; :: thesis: verum