let
a
,
b
be
FinSequence
;
:: thesis:
( (
a
^
b
=
a
or
b
^
a
=
a
) implies
b
=
{}
)
assume
A1
: (
a
^
b
=
a
or
b
^
a
=
a
) ;
:: thesis:
b
=
{}
per
cases
(
a
^
b
=
a
or
b
^
a
=
a
)
by
A1
;
suppose
A2
:
a
^
b
=
a
;
:: thesis:
b
=
{}
len
(
a
^
b
)
=
(
len
a
)
+
(
len
b
)
by
FINSEQ_1:22
;
hence
b
=
{}
by
A2
;
:: thesis:
verum
end;
suppose
A3
:
b
^
a
=
a
;
:: thesis:
b
=
{}
len
(
b
^
a
)
=
(
len
b
)
+
(
len
a
)
by
FINSEQ_1:22
;
hence
b
=
{}
by
A3
;
:: thesis:
verum
end;
end;