let fp be FinSequence of NAT ; for n being Element of NAT
for a being Nat st len fp = n + 1 & a >= 1 & a <= n holds
(Del (fp,a)) . n = fp . (len fp)
let n be Element of NAT ; for a being Nat st len fp = n + 1 & a >= 1 & a <= n holds
(Del (fp,a)) . n = fp . (len fp)
let a be Nat; ( len fp = n + 1 & a >= 1 & a <= n implies (Del (fp,a)) . n = fp . (len fp) )
assume that
A1:
len fp = n + 1
and
A2:
a >= 1
and
A3:
a <= n
; (Del (fp,a)) . n = fp . (len fp)
n < n + 1
by XREAL_1:29;
then
a < n + 1
by A3, XXREAL_0:2;
then
a in dom fp
by A1, A2, FINSEQ_3:25;
hence
(Del (fp,a)) . n = fp . (len fp)
by A1, A3, WSIERP_1:def 1; verum