let n be Nat; :: thesis: for p being XFinSequence st len p = n + 1 holds
p = (p | n) ^ <%(p . n)%>
let p be XFinSequence; :: thesis: ( len p = n + 1 implies p = (p | n) ^ <%(p . n)%> )
set pn = p | n;
set x = p . n;
assume A1: len p = n + 1 ; :: thesis: p = (p | n) ^ <%(p . n)%>
then A2: n < len p by NAT_1:13;
then A3: len (p | n) = n by Th51;

A4: now :: thesis: for m being Nat st m in dom p holds
p . m = ((p | n) ^ <%(p . n)%>) . m

let m be Nat; :: thesis: ( m in dom p implies p . m = ((p | n) ^ <%(p . n)%>) . m )
assume m in dom p ; :: thesis: p . m = ((p | n) ^ <%(p . n)%>) . m
then m < len p by Lm1;
then A5: m <= len (p | n) by A1, A3, NAT_1:13;

now :: thesis: ( ( m = len (p | n) & p . m = ((p | n) ^ <%(p . n)%>) . m ) or ( m <> len (p | n) & ((p | n) ^ <%(p . n)%>) . m = p . m ) )

per cases ( m = len (p | n) or m <> len (p | n) ) ;

case m = len (p | n) ; :: thesis: p . m = ((p | n) ^ <%(p . n)%>) . m

hence p . m = ((p | n) ^ <%(p . n)%>) . m by A3, Th33; :: thesis: verum

end;

case m <> len (p | n) ; :: thesis: ((p | n) ^ <%(p . n)%>) . m = p . m

then m < len (p | n) by A5, XXREAL_0:1;
then A6: m in dom (p | n) by Lm1;
hence ((p | n) ^ <%(p . n)%>) . m = (p | n) . m by Def3
.= p . m by A2, A3, A6, Th50 ;
:: thesis: verum

end;

end;

end;

hence p . m = ((p | n) ^ <%(p . n)%>) . m ; :: thesis: verum

end;

len ((p | n) ^ <%(p . n)%>) = n + (len <%(p . n)%>) by A3, Def3
.= len p by A1, Def4 ;
hence p = (p | n) ^ <%(p . n)%> by A4; :: thesis: verum