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;
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 :: thesis: 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 ; :: 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 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 } ; :: thesis: verum

end;

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

now :: thesis: 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 ; :: 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
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; :: thesis: 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; :: thesis: verum