let n be Nat; :: thesis: for f being Complex_Sequence holds (XProduct (f | n)) * (f . n) = XProduct (f | (n + 1))
let f be Complex_Sequence; :: thesis: (XProduct (f | n)) * (f . n) = XProduct (f | (n + 1))
reconsider g = f | (n + 1) as complex-valued XFinSequence ;
n + 0 < n + 1 by XREAL_1:6;
then A1: n in dom g by AFINSQ_1:86;
then XProduct (g | (n + 1)) = (XProduct (g | n)) * (g . n) by A265
.= (XProduct (f | ((n + 1) /\ n))) * ((f | (n + 1)) . n) by RELAT_1:71
.= (XProduct (f | n)) * ((f | (n + 1)) . n) ;
hence (XProduct (f | n)) * (f . n) = XProduct (f | (n + 1)) by A1, FUNCT_1:47; :: thesis: verum