let n be Nat; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: (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; :: thesis: verum