let D be non empty set ; :: thesis: for x being set
for f being FinSequence of D st 1 <= len f holds
( (f ^ <*x*>) . 1 = f . 1 & (f ^ <*x*>) . 1 = f /. 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) & (<*x*> ^ f) . ((len f) + 1) = f /. (len f) )
let x be set ; :: thesis: for f being FinSequence of D st 1 <= len f holds
( (f ^ <*x*>) . 1 = f . 1 & (f ^ <*x*>) . 1 = f /. 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) & (<*x*> ^ f) . ((len f) + 1) = f /. (len f) )
let f be FinSequence of D; :: thesis: ( 1 <= len f implies ( (f ^ <*x*>) . 1 = f . 1 & (f ^ <*x*>) . 1 = f /. 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) & (<*x*> ^ f) . ((len f) + 1) = f /. (len f) ) )
assume A1: 1 <= len f ; :: thesis: ( (f ^ <*x*>) . 1 = f . 1 & (f ^ <*x*>) . 1 = f /. 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) & (<*x*> ^ f) . ((len f) + 1) = f /. (len f) )
then A2: len f in dom f by FINSEQ_3:25;
1 in dom f by A1, FINSEQ_3:25;
then A3: (f ^ <*x*>) . 1 = f . 1 by FINSEQ_1:def 7;
(<*x*> ^ f) . ((len f) + 1) = (<*x*> ^ f) . ((len <*x*>) + (len f)) by FINSEQ_1:39
.= f . (len f) by A2, FINSEQ_1:def 7 ;
hence ( (f ^ <*x*>) . 1 = f . 1 & (f ^ <*x*>) . 1 = f /. 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) & (<*x*> ^ f) . ((len f) + 1) = f /. (len f) ) by A1, A3, FINSEQ_4:15; :: thesis: verum