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
len f <> 0 by A2;
then A3: 1 <= len f by NAT_1:14;
( n <= len f implies len (f | n) = n ) by FINSEQ_1:80;
then 1 <= len (f | n) by A1, A3, FINSEQ_1:79;
then 1 in dom (f | n) by FINSEQ_3:27;
hence (Ins f,n,p) /. 1 = f /. 1 by Th75; :: thesis: verum