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

proof

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

end;

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