let fp be FinSequence of NAT ; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: (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; :: thesis: verum