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

proof

let x be set ; :: 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 A2, Th96
.= <*b*> . x by A5, FINSEQ_1:def 8 ;
:: thesis: verum

end;

hence <*a*> +* 1,b = <*b*> by A3, A4, FUNCT_1:9; :: thesis: verum