let a, b be set ; :: thesis: <*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

proof

let x be object ; :: thesis: ( x in {1} implies (<*a*> +* (1,b)) . x = <*b*> . x )
assume x in {1} ; :: thesis: (<*a*> +* (1,b)) . x = <*b*> . x
then A5: x = 1 by TARSKI:def 1;
hence (<*a*> +* (1,b)) . x = b by A3, Th93
.= <*b*> . x by A5 ;
:: thesis: verum

end;

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; :: thesis: verum