let x be set ; :: thesis: for f being FinSequence holds
( len (f ^ <*x*>) = (len f) + 1 & len (<*x*> ^ f) = (len f) + 1 & (f ^ <*x*>) . ((len f) + 1) = x & (<*x*> ^ f) . 1 = x )
let f be FinSequence; :: thesis: ( len (f ^ <*x*>) = (len f) + 1 & len (<*x*> ^ f) = (len f) + 1 & (f ^ <*x*>) . ((len f) + 1) = x & (<*x*> ^ f) . 1 = x )
A1: len (<*x*> ^ f) = (len <*x*>) + (len f) by FINSEQ_1:35
.= (len f) + 1 by FINSEQ_1:56 ;
( 1 <= 1 & 1 <= len <*x*> ) by FINSEQ_1:56;
then A2: 1 in dom <*x*> by FINSEQ_3:27;
then A3: (f ^ <*x*>) . ((len f) + 1) = <*x*> . 1 by FINSEQ_1:def 7
.= x by FINSEQ_1:def 8 ;
(<*x*> ^ f) . 1 = <*x*> . 1 by A2, FINSEQ_1:def 7
.= x by FINSEQ_1:def 8 ;
hence ( len (f ^ <*x*>) = (len f) + 1 & len (<*x*> ^ f) = (len f) + 1 & (f ^ <*x*>) . ((len f) + 1) = x & (<*x*> ^ f) . 1 = x ) by A1, A3, FINSEQ_2:19; :: thesis: verum