let x, y be object ; :: thesis: <%x%> +~ (x,y) = <%y%>
A1: dom (<%x%> +~ (x,y)) = dom <%x%> by FUNCT_4:99
.= Segm 1 by Th30 ;
then <%x%> +~ (x,y) is finite by FINSET_1:10;
then reconsider p = <%x%> +~ (x,y) as XFinSequence by A1, ORDINAL1:def 7;
A2: rng <%x%> = {x} by Th30;
then rng p c= ({x} \ {x}) \/ {y} by FUNCT_4:104;
then rng p c= {} \/ {y} by XBOOLE_1:37;
then A3: rng p c= {y} ;
x in rng <%x%> by A2, TARSKI:def 1;
then y in rng p by FUNCT_4:101;
hence <%x%> +~ (x,y) = <%y%> by A1, Th30, A3, ZFMISC_1:33; :: thesis: verum