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

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) ) )

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

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

end;

assume [a,b] in id {{} } ; :: thesis: [a,b] in the InternalRel of (product J)
then A3: ( a in {{} } & a = b ) by RELAT_1:def 10;
then A4: a = {} by TARSKI:def 1;
reconsider x = {} , y = {} as Element of (product J) by A1, TARSKI:def 1;
( x = {} --> {{} } & y = {} --> {{} } ) ;
then reconsider f = x, g = y as Function ;
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 x <= y by A1, A2, Def4;
hence [a,b] in the InternalRel of (product J) by A3, A4, ORDERS_2:def 9; :: thesis: verum

end;

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