let J be RelStr-yielding ManySortedSet of {} ; :: thesis: product J = RelStr(# {{}},(id {{}}) #)
set IT = product J;
A1: the carrier of (product J) = product (Carrier J) by Def4
.= {{}} by CARD_3:10, PBOOLE:122 ;
A2: product (Carrier J) = {{}} by CARD_3:10, PBOOLE:122;
the InternalRel of (product J) = id {{}}

proof

reconsider x = {} , y = {} as Element of (product J) by A1, TARSKI:def 1;
let a, b be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [a,b] in the InternalRel of (product J) or [a,b] in id {{}} ) & ( not [a,b] in id {{}} or [a,b] in the InternalRel of (product J) ) )
x = {} --> {{}} ;
then reconsider f = x, g = y as Function ;

hereby :: thesis: ( not [a,b] in id {{}} or [a,b] in the InternalRel of (product J) )

assume A3: [a,b] in the InternalRel of (product J) ; :: thesis: [a,b] in id {{}}
then A4: b in the carrier of (product J) by ZFMISC_1:87;
A5: a in the carrier of (product J) by A3, ZFMISC_1:87;
then a = {} by A1, TARSKI:def 1;
then a = b by A1, A4, TARSKI:def 1;
hence [a,b] in id {{}} by A1, A5, RELAT_1:def 10; :: thesis: verum

end;

assume A6: [a,b] in id {{}} ; :: thesis: [a,b] in the InternalRel of (product J)
then a in {{}} by RELAT_1:def 10;
then A7: a = {} by TARSKI:def 1;
for i being object st i in {} holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ;
then A8: x <= y by A1, A2, Def4;
a = b by A6, RELAT_1:def 10;
hence [a,b] in the InternalRel of (product J) by A7, A8, ORDERS_2:def 5; :: thesis: verum

end;

hence product J = RelStr(# {{}},(id {{}}) #) by A1; :: thesis: verum