per
cases
(
x
in
dom
p
or not
x
in
dom
p
)
;
suppose
x
in
dom
p
;
:: thesis:
p
.
x
is
Sequence-like
hence
p
.
x
is
Sequence-like
by
Def1
;
:: thesis:
verum
end;
suppose
not
x
in
dom
p
;
:: thesis:
p
.
x
is
Sequence-like
hence
p
.
x
is
Sequence-like
by
FUNCT_1:def 2
;
:: thesis:
verum
end;
end;