let X be non-empty non empty FinSequence; for Y being non empty set ex K being Function of [:(product X),Y:],(product (X ^ <*Y*>)) st
( K is bijective & ( for x being FinSequence
for y being object st x in product X & y in Y holds
K . (x,y) = x ^ <*y*> ) )
let Y be non empty set ; ex K being Function of [:(product X),Y:],(product (X ^ <*Y*>)) st
( K is bijective & ( for x being FinSequence
for y being object st x in product X & y in Y holds
K . (x,y) = x ^ <*y*> ) )
consider I being Function of [:(product X),Y:],[:(product X),(product <*Y*>):] such that
A1:
( I is bijective & ( for x, y being object st x in product X & y in Y holds
I . (x,y) = [x,<*y*>] ) )
by Th4;
consider J being Function of [:(product X),(product <*Y*>):],(product (X ^ <*Y*>)) such that
A2:
( J is one-to-one & J is onto & ( for x, y being FinSequence st x in product X & y in product <*Y*> holds
J . (x,y) = x ^ y ) )
by PRVECT_3:6;
set K = J * I;
reconsider K = J * I as Function of [:(product X),Y:],(product (X ^ <*Y*>)) ;
take
K
; ( K is bijective & ( for x being FinSequence
for y being object st x in product X & y in Y holds
K . (x,y) = x ^ <*y*> ) )
A3:
rng J = product (X ^ <*Y*>)
by A2, FUNCT_2:def 3;
rng I = [:(product X),(product <*Y*>):]
by A1, FUNCT_2:def 3;
then rng (J * I) =
J .: [:(product X),(product <*Y*>):]
by RELAT_1:127
.=
product (X ^ <*Y*>)
by A3, RELSET_1:22
;
then
K is onto
by FUNCT_2:def 3;
hence
K is bijective
by A1, A2; for x being FinSequence
for y being object st x in product X & y in Y holds
K . (x,y) = x ^ <*y*>
thus
for x being FinSequence
for y being object st x in product X & y in Y holds
K . (x,y) = x ^ <*y*>
verumproof
let x be
FinSequence;
for y being object st x in product X & y in Y holds
K . (x,y) = x ^ <*y*>let y be
object ;
( x in product X & y in Y implies K . (x,y) = x ^ <*y*> )
assume A4:
(
x in product X &
y in Y )
;
K . (x,y) = x ^ <*y*>
then A5:
I . (
x,
y)
= [x,<*y*>]
by A1;
[x,y] in [:(product X),Y:]
by A4, ZFMISC_1:87;
then
I . [x,y] in [:(product X),(product <*Y*>):]
by FUNCT_2:5;
then
<*y*> in product <*Y*>
by A5, ZFMISC_1:87;
then
J . (
x,
<*y*>)
= x ^ <*y*>
by A4, A2;
hence
K . (
x,
y)
= x ^ <*y*>
by A5, A4, ZFMISC_1:87, FUNCT_2:15;
verum
end;