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