let n be Nat; :: thesis: for f being complex-valued XFinSequence st n in dom f holds
(XProduct (f | n)) * (f . n) = XProduct (f | (n + 1))
let f be complex-valued XFinSequence; :: thesis: ( n in dom f implies (XProduct (f | n)) * (f . n) = XProduct (f | (n + 1)) )
assume A1: n in dom f ; :: thesis: (XProduct (f | n)) * (f . n) = XProduct (f | (n + 1))
reconsider f1 = f as XFinSequence of COMPLEX ;
multcomplex . ((multcomplex "**" (f | n)),(f . n)) = multcomplex "**" (f | (n + 1)) by A1, AFINSQ_2:43;
hence (XProduct (f | n)) * (f . n) = XProduct (f | (n + 1)) by BINOP_2:def 5; :: thesis: verum