let f be XFinSequence; :: thesis: for n being Element of NAT st len f = n + 1 holds
f = (f | n) ^ <%(f . n)%>
let n be Element of NAT ; :: thesis: ( len f = n + 1 implies f = (f | n) ^ <%(f . n)%> )
set fn = f | n;
set x = f . n;
assume A1: len f = n + 1 ; :: thesis: f = (f | n) ^ <%(f . n)%>
then A2: len (f | n) = n by Th12, NAT_1:11;
A3: n < len f by A1, NAT_1:13;

A4: now

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

now

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

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

hence f . m = ((f | n) ^ <%(f . n)%>) . m by A2, AFINSQ_1:40; :: thesis: verum

end;

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

then m < len (f | n) by A5, XXREAL_0:1;
then A6: m in dom (f | n) by NAT_1:45;
hence ((f | n) ^ <%(f . n)%>) . m = (f | n) . m by AFINSQ_1:def 4
.= f . m by A3, A2, A6, Th11 ;
:: thesis: verum

end;

end;

end;

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

end;

len ((f | n) ^ <%(f . n)%>) = n + (len <%(f . n)%>) by A2, AFINSQ_1:20
.= len f by A1, AFINSQ_1:38 ;
hence f = (f | n) ^ <%(f . n)%> by A4, Th5; :: thesis: verum