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:19, PBOOLE:134 ;
A2: product (Carrier J) = {{} } by CARD_3:19, PBOOLE:134;
the InternalRel of (product J) = id {{} }

proof

reconsider x = {} , y = {} as Element of (product J) by A1, TARSKI:def 1;
let a, b be set ; :: 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:106;
A5: a in the carrier of (product J) by A3, ZFMISC_1:106;
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 set 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 9; :: thesis: verum

end;

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