let U be non empty set ; :: thesis: (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;
B2: 1 -tuples_on U = { <*u*> where u is Element of U : verum } by FINSEQ_2:96;
B0: ( dom (id (1 -tuples_on U)) = 1 -tuples_on U & dom (U -concatenation) = [:(U *),(U *):] ) by FUNCT_2:def 1;
then B1: 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

let y be set ; :: thesis: ( 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)) ; :: thesis: y in { <*u,u*> where u is Element of U : verum }
then consider x being set such that
C0: ( 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
C2: ( x = [p,((id (1 -tuples_on U)) . p)] & p in 1 -tuples_on U ) by C0, B1;
consider u being Element of U such that
C3: p = <*u*> by C2, B2;
reconsider pp = p as FinSequence of U ;
{((id (1 -tuples_on U)) . p)} \ {p} is empty ;
then y = (U -concatenation) . (pp,pp) by C0, C2, ZFMISC_1:15;
then y = <*u,u*> by Th4, C3;
hence y in { <*u,u*> where u is Element of U : verum } ; :: thesis: verum

end;

then B3: (U -concatenation) .: (id (1 -tuples_on U)) c= { <*u,u*> where u is Element of U : verum } by TARSKI:def 3;

now

let y be set ; :: thesis: ( 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 } ; :: thesis: y in (U -concatenation) .: (id (1 -tuples_on U))
then consider u being Element of U such that
C0: 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 ) by FUNCT_1:18;
then [p,p] in id (1 -tuples_on U) by B1;
then reconsider dd = [p,p] as Element of id (1 -tuples_on U) ;
Z0: dd in DD null [:(U *),(U *):] ;
y = (U -concatenation) . (pp,pp) by C0, Th4
.= (U -concatenation) . dd ;
hence y in (U -concatenation) .: (id (1 -tuples_on U)) by Z0, B0, FUNCT_1:def 6; :: thesis: verum

end;

then { <*u,u*> where u is Element of U : verum } c= (U -concatenation) .: (id (1 -tuples_on U)) by TARSKI:def 3;
hence (U -concatenation) .: (id (1 -tuples_on U)) = { <*u,u*> where u is Element of U : verum } by B3, XBOOLE_0:def 10; :: thesis: verum