let x be object ; :: thesis: for p being XFinSequence holds CutLastLoc (p ^ <%x%>) = p
let p be XFinSequence; :: thesis: CutLastLoc (p ^ <%x%>) = p
set q = CutLastLoc (p ^ <%x%>);
A1: (len (p ^ <%x%>)) -' 1 = ((len p) + 1) -' 1 by AFINSQ_1:75
.= len p by NAT_D:34 ;
A2: dom (p ^ <%x%>) = len (p ^ <%x%>)
.= Segm ((len p) + 1) by AFINSQ_1:75
.= (Segm (len p)) \/ {(len p)} by AFINSQ_1:2 ;
A3: not len p in dom p ;
LastLoc (p ^ <%x%>) = (len (p ^ <%x%>)) -' 1 by AFINSQ_1:70;
hence A4: dom (CutLastLoc (p ^ <%x%>)) = (dom (p ^ <%x%>)) \ {(len p)} by A1, VALUED_1:36
.= dom p by A2, A3, ZFMISC_1:117 ;
:: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (CutLastLoc (p ^ <%x%>)) or (CutLastLoc (p ^ <%x%>)) . b₁ = p . b₁ )
let y be object ; :: thesis: ( not y in dom (CutLastLoc (p ^ <%x%>)) or (CutLastLoc (p ^ <%x%>)) . y = p . y )
assume A5: y in dom (CutLastLoc (p ^ <%x%>)) ; :: thesis: (CutLastLoc (p ^ <%x%>)) . y = p . y
A6: p c= p ^ <%x%> by AFINSQ_1:74;
thus (CutLastLoc (p ^ <%x%>)) . y = (p ^ <%x%>) . y by A5, GRFUNC_1:2
.= p . y by A5, A4, A6, GRFUNC_1:2 ; :: thesis: verum