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 A3: n < len p by NAT_1:13;
then A2: len (p | n) = n by Th121;

A4: now

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 NAT_1:45;
then A5: m <= len (p | n) by A1, A2, NAT_1:13;

now

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 A2, Th40; :: 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 NAT_1:45;
hence ((p | n) ^ <%(p . n)%>) . m = (p | n) . m by Def4
.= p . m by A3, A2, A6, Th111 ;
:: 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 A2, Def4
.= len p by A1, Def5 ;
hence p = (p | n) ^ <%(p . n)%> by A4, Th10; :: thesis: verum