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

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