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

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