let x be object ; :: thesis: for n being Nat
for f being FinSequence st n in dom f holds
(<*x*> ^ f) . (n + 1) = f . n
let n be Nat; :: thesis: for f being FinSequence st n in dom f holds
(<*x*> ^ f) . (n + 1) = f . n
let f be FinSequence; :: thesis: ( n in dom f implies (<*x*> ^ f) . (n + 1) = f . n )
len <*x*> = 1 by FINSEQ_1:39;
hence ( n in dom f implies (<*x*> ^ f) . (n + 1) = f . n ) by FINSEQ_1:def 7; :: thesis: verum