let a, b be set ; <*a*> +* (1,b) = <*b*>
A1:
dom <*b*> = {1}
by FINSEQ_1:2, FINSEQ_1:def 8;
A2:
dom <*a*> = {1}
by FINSEQ_1:2, FINSEQ_1:def 8;
then
1 in dom <*a*>
by TARSKI:def 1;
then A3:
<*a*> +* (1,b) = <*a*> +* (1 .--> b)
by Def2;
A4:
for x being object st x in {1} holds
(<*a*> +* (1,b)) . x = <*b*> . x
dom (<*a*> +* (1,b)) =
(dom <*a*>) \/ (dom (1 .--> b))
by A3, FUNCT_4:def 1
.=
{1} \/ {1}
by A2
.=
{1}
;
hence
<*a*> +* (1,b) = <*b*>
by A1, A4; verum