thus ( S <> {} implies |.S.| is ManySortedSet of I ) :: thesis: ( not S <> {} implies [[0]] I is ManySortedSet of I )

proof

assume S <> {} ; :: thesis: |.S.| is ManySortedSet of I
then dom |.S.| = I by Th14;
hence |.S.| is ManySortedSet of I by PARTFUN1:def 4, RELAT_1:def 18; :: thesis: verum

end;

thus ( not S <> {} implies [[0]] I is ManySortedSet of I ) ; :: thesis: verum