let x be set ; :: thesis: for p being XFinSequence holds CutLastLoc (p ^ <%x%>) = p
let p be XFinSequence; :: thesis: CutLastLoc (p ^ <%x%>) = p
set q = CutLastLoc (p ^ <%x%>);
A: (len (p ^ <%x%>)) -' 1 = ((len p) + 1) -' 1 by AFINSQ_1:75
.= len p by NAT_D:34 ;
B: dom (p ^ <%x%>) = len (p ^ <%x%>)
.= (len p) + 1 by AFINSQ_1:75
.= (dom p) \/ {(len p)} by AFINSQ_1:2 ;
C: not len p in dom p ;
LastLoc (p ^ <%x%>) = (len (p ^ <%x%>)) -' 1 by AFINSQ_1:70;
hence K: dom (CutLastLoc (p ^ <%x%>)) = (dom (p ^ <%x%>)) \ {(len p)} by A, VALUED_1:36
.= dom p by B, C, ZFMISC_1:117 ;
:: according to FUNCT_1:def 11 :: thesis: for b₁ being set holds
( not b₁ in proj1 (CutLastLoc (p ^ <%x%>)) or (CutLastLoc (p ^ <%x%>)) . b₁ = p . b₁ )
let y be set ; :: thesis: ( not y in proj1 (CutLastLoc (p ^ <%x%>)) or (CutLastLoc (p ^ <%x%>)) . y = p . y )
assume Z: y in dom (CutLastLoc (p ^ <%x%>)) ; :: thesis: (CutLastLoc (p ^ <%x%>)) . y = p . y
D: p c= p ^ <%x%> by AFINSQ_1:74;
CutLastLoc (p ^ <%x%>) c= p ^ <%x%> by XBOOLE_1:36;
hence (CutLastLoc (p ^ <%x%>)) . y = (p ^ <%x%>) . y by Z, GRFUNC_1:2
.= p . y by Z, K, D, GRFUNC_1:2 ;
:: thesis: verum