let n be Nat; for D being non empty set
for p being Element of D
for f being FinSequence of D st 1 <= n & not f is empty holds
(Ins (f,n,p)) . 1 = f . 1
let D be non empty set ; for p being Element of D
for f being FinSequence of D st 1 <= n & not f is empty holds
(Ins (f,n,p)) . 1 = f . 1
let p be Element of D; for f being FinSequence of D st 1 <= n & not f is empty holds
(Ins (f,n,p)) . 1 = f . 1
let f be FinSequence of D; ( 1 <= n & not f is empty implies (Ins (f,n,p)) . 1 = f . 1 )
assume that
A1:
1 <= n
and
A2:
not f is empty
; (Ins (f,n,p)) . 1 = f . 1
A3:
( n <= len f implies len (f | n) = n )
by FINSEQ_1:59;
1 <= len f
by A2, NAT_1:14;
then
1 <= len (f | n)
by A1, A3, FINSEQ_1:58;
then
1 in dom (f | n)
by FINSEQ_3:25;
hence
(Ins (f,n,p)) . 1 = f . 1
by Th72; verum