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