let
S
be
void
ManySortedSign
;
:: thesis:
id
the
carrier
of
S
,
id
the
carrier'
of
S
form_morphism_between
S
,
S
per
cases
(
S
is
empty
or not
S
is
empty
)
;
suppose
S
is
empty
;
:: thesis:
id
the
carrier
of
S
,
id
the
carrier'
of
S
form_morphism_between
S
,
S
hence
id
the
carrier
of
S
,
id
the
carrier'
of
S
form_morphism_between
S
,
S
by
Lm1
;
:: thesis:
verum
end;
suppose
not
S
is
empty
;
:: thesis:
id
the
carrier
of
S
,
id
the
carrier'
of
S
form_morphism_between
S
,
S
hence
id
the
carrier
of
S
,
id
the
carrier'
of
S
form_morphism_between
S
,
S
by
Lm2
;
:: thesis:
verum
end;
end;