let U be non empty set ; (U -concatenation) .: (id (1 -tuples_on U)) = { <*u,u*> where u is Element of U : verum }
set f = U -concatenation ;
set U1 = 1 -tuples_on U;
set D = id (1 -tuples_on U);
set U2 = 2 -tuples_on U;
set A = (U -concatenation) .: (id (1 -tuples_on U));
set B = { <*u,u*> where u is Element of U : verum } ;
( id (1 -tuples_on U) c= [:(1 -tuples_on U),(1 -tuples_on U):] & 1 -tuples_on U c= U * )
by FINSEQ_2:142;
then
[:(1 -tuples_on U),(1 -tuples_on U):] c= [:(U *),(U *):]
by ZFMISC_1:96;
then reconsider DD = id (1 -tuples_on U) as Subset of [:(U *),(U *):] by XBOOLE_1:1;
A1:
1 -tuples_on U = { <*u*> where u is Element of U : verum }
by FINSEQ_2:96;
A2:
( dom (id (1 -tuples_on U)) = 1 -tuples_on U & dom (U -concatenation) = [:(U *),(U *):] )
by FUNCT_2:def 1;
then A3:
id (1 -tuples_on U) = { [x,((id (1 -tuples_on U)) . x)] where x is Element of 1 -tuples_on U : x in 1 -tuples_on U }
by Th20;
now for y being object st y in (U -concatenation) .: (id (1 -tuples_on U)) holds
y in { <*u,u*> where u is Element of U : verum } let y be
object ;
( y in (U -concatenation) .: (id (1 -tuples_on U)) implies y in { <*u,u*> where u is Element of U : verum } )assume
y in (U -concatenation) .: (id (1 -tuples_on U))
;
y in { <*u,u*> where u is Element of U : verum } then consider x being
object such that A4:
(
x in dom (U -concatenation) &
x in id (1 -tuples_on U) &
y = (U -concatenation) . x )
by FUNCT_1:def 6;
consider p being
Element of 1
-tuples_on U such that A5:
(
x = [p,((id (1 -tuples_on U)) . p)] &
p in 1
-tuples_on U )
by A4, A3;
consider u being
Element of
U such that A6:
p = <*u*>
by A5, A1;
reconsider pp =
p as
FinSequence of
U ;
y = (U -concatenation) . (
pp,
pp)
by A4, A5;
then
y = <*u,u*>
by Th4, A6;
hence
y in { <*u,u*> where u is Element of U : verum }
;
verum end;
then A7:
(U -concatenation) .: (id (1 -tuples_on U)) c= { <*u,u*> where u is Element of U : verum }
;
now for y being object st y in { <*u,u*> where u is Element of U : verum } holds
y in (U -concatenation) .: (id (1 -tuples_on U))let y be
object ;
( y in { <*u,u*> where u is Element of U : verum } implies y in (U -concatenation) .: (id (1 -tuples_on U)) )assume
y in { <*u,u*> where u is Element of U : verum }
;
y in (U -concatenation) .: (id (1 -tuples_on U))then consider u being
Element of
U such that A8:
y = <*u,u*>
;
reconsider p =
<*u*> as
Element of 1
-tuples_on U by FINSEQ_2:98;
reconsider pp =
p as
FinSequence of
U ;
(
[p,((id (1 -tuples_on U)) . p)] = [p,p] &
p in 1
-tuples_on U )
;
then
[p,p] in id (1 -tuples_on U)
by A3;
then reconsider dd =
[p,p] as
Element of
id (1 -tuples_on U) ;
A9:
dd in DD null [:(U *),(U *):]
;
y =
(U -concatenation) . (
pp,
pp)
by A8, Th4
.=
(U -concatenation) . dd
;
hence
y in (U -concatenation) .: (id (1 -tuples_on U))
by A9, A2, FUNCT_1:def 6;
verum end;
then
{ <*u,u*> where u is Element of U : verum } c= (U -concatenation) .: (id (1 -tuples_on U))
;
hence
(U -concatenation) .: (id (1 -tuples_on U)) = { <*u,u*> where u is Element of U : verum }
by A7; verum